# proposal/20-guarded-feedback.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/cec995bda40918ae3d1538fa061eec6714699600/proposal/20-guarded-feedback.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: cec995bda40918ae3d1538fa061eec6714699600

Requested commit: cec995bda40918ae3d1538fa061eec6714699600

Commit: cec995bda40918ae3d1538fa061eec6714699600

Blob: 2069a590bda09f49a90826088745b4dfb08a5bba

Size: 35373 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/cec995bda40918ae3d1538fa061eec6714699600/proposal/20-guarded-feedback.md?format=markdown)

````
# Guarded Feedback (`delay`/`Later<Clock, T>`, v0)

What `delay`/`Later<Clock, T>` are as a checked construct, the smallest real slice of guarded feedback that is soundly buildable now, whether `reg <- expr` already is an informal version of this judgment (it is not — see §2), and the FIX-ω resolution D-093 §7 and D-094 §5/§7 both named as a binding obligation and explicitly declined to make — made here, not deferred a third time. Principles in force: P-1 (no implicit behavior), P-2 (cost visible), P-3 (meaning survives lowering), P-9 (diagnostics name their judgment). This doc is the `later`/feedback slice of D-010's stratified judgment that [17](17-memory-model.md) leaned on informally and [18](18-grade-system.md)/[19](19-linearity.md) both fenced off as the one interaction their v0s could not reach.

## Committed design

### 1. What's specified vs. what exists in code, re-verified

[03 §5](03-time-and-resources.md) (D-013, D-029) commits the construct precisely: **"a register is `delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>>`; feedback is legal only through `Later`."** `next` is an ordinary expression, re-evaluated every cycle — this is guarded feedback in the Nakano/Guarded-Cubical-Agda sense (a `▷`/"later" modality guarding recursive occurrences so a fixed point is only well-founded if every self-reference is delayed by at least one step), but D-013 is explicit that Strata ships only the *unary* case — `later` = "next cycle in this clock domain" — not the general ∀κ-quantified guarded recursion of the proof-assistant literature: "the unary case — `later` = 'next cycle in this domain' — is far simpler [than full clocked type theory]... Multi-clock guarded quantification (∀κ) is DEFERRED." The comparison point named directly is Clash, where a register-free feedback loop *type-checks* and only fails at simulation-divergence or synthesis-time-combinational-loop time; Strata's committed improvement is that an unguarded cycle is rejected **compositionally** — a component's feedback port demands `Later<_, T>` in its own signature, so causality safety is visible from the signature alone, without opening the body (D-013 calls this out as "critical for agent composition"). A post-elaboration graph check remains as a backstop for whatever the signature-level check cannot see.

D-029's soundness content is FIX-ω, and §5's own text gives its shape directly, not just an English gloss layered on top: **"the feedback rule requires FIX-ω: usage inside a feedback body is ω-promoted, because feedback re-executes every cycle and the naive rule let a 1-graded value be spent once *per cycle*, a bug neither QTT nor guarded recursion alone can express."** The corollary D-013 records as "load-bearing and pleasant" is the reconciliation: **ω-graded periodic capabilities (initiation intervals, [03 §3](03-time-and-resources.md)) remain usable in feedback — II is precisely how linearity reconciles with per-cycle reuse.** This is the closest thing D-013 gives to a formal type rule; the wave-2 core-calculus probe ([open-problems.md](open-problems.md) OP-7) that found the bug and proved the fix lives in `probes/core-calculus/`'s λ-strata⁰ fragment (23 typing + 4 WF rules), not in this doc's source tree — OP-7's entry records the finding ("the naive feedback rule accepts a 1-graded value spent once per cycle... fixed by FIX-ω (ω-promotion of feedback-body usage)") and its status as one of two GAPS-FOUND-and-repaired cross-discipline unsoundnesses in the phase-1/2 fragment, both now closed at the calculus level. What OP-7 does *not* give is an implementation-level algorithm against this codebase's actual `linear_uses`/`UseCount` shape — that is this doc's job, done in §5.

**Re-verifying the zero-representation claim, directly.** `grep -n "\"delay\"\|Later\|guarded\|feedback" crates/strata-syntax/src/parser.rs crates/strata-hir/src/lib.rs crates/strata-check/src/lib.rs` returns **nothing** — confirmed again here, third time this project has run this exact grep (D-093 §7, D-094 §5, now this doc) and gotten the identical empty result. `find . -iname "*.strata" | xargs grep -ln "delay"` and `grep -rn "delay\|Later" fixtures/` also return nothing: **no fixture in the corpus uses `delay`, guarded feedback, or anything `Later`-shaped.** This is a real divergence from every prior doc in this series. D-092's `mem` was forced by `fifo.strata`'s same-cycle push/pop; D-094's `linear let` was scoped against a construct ([04](04-protocols-and-streams.md)'s capability tokens) that at least has a named motivating shape even without a fixture. `delay`/`Later` has neither a fixture nor an existing partially-parsing surface (`ghost`'s situation before D-093, or `linear`'s absence before D-094 — this is the *same* absence, but this time there is also no forcing example anywhere in the corpus to scope against). The honest finding this doc must state plainly, matching the "smallest real forced slice" discipline every prior doc in this series used: **nothing in the current corpus forces a specific shape for `delay`/`Later`.** This doc's v0 is scoped directly off D-013/D-029's own committed signature instead — the only concrete evidence source available — not off a fixture, because none exists. §2 makes this scoping decision explicit rather than pretending a fixture-forced answer exists.

### 2. The central architectural question, resolved directly: `reg <- expr` is not an informal `Later` judgment

A plausible hypothesis, worth checking before designing anything new: maybe `delay`/`Later` is not a new primitive at all, but the formal typing story that *justifies* why `reg name <- expr;` (D-079, already implemented, already lowering to `seq.firreg` today) is sound — in which case v0 might mean "make `RegisterUpdate` checking go through a real `Later`-typed judgment" rather than "add `delay(...)` from scratch."

**Checked directly against `crates/strata-check/src/lib.rs`'s `StatementKind::RegisterUpdate` handling (~line 2773) — the hypothesis is false. Register-update checking is not, even informally, a `Later`-typed judgment.** What actually happens: `target`'s existing type `want` (the register's plain element type `T`, not `Later<Clock, T>` or any modally-wrapped type) is looked up, `value` is checked with `self.expr(value, true, Some(&want))`, and the result is compared for type equality against `want` via `types_equal` — ordinary same-cycle type checking, the identical code path used for `let` initializers and component outputs. There is no `Later<_, _>` type anywhere in `TypeKind` (§1's grep already established this), no separate "next-cycle" type distinct from `T` that `value` is checked against, and no modal wrapper stripped or introduced anywhere in this function. The only place D-092/D-093 gesture at "the guarded-feedback vocabulary" is the `reject_if_tainted` **skip**: a register update's value slot is the one place `mem_tainted` values are deliberately *not* rejected ("this is the one legal latency-boundary crossing... No `reject_if_tainted` call, deliberately"). That is a single boolean bypass in an unrelated taint pass (D-092's `mem`-read-latency bookkeeping), not a modal type judgment — it encodes "you're allowed to let a one-cycle-delayed value settle here," which is necessary but nowhere near sufficient for what `Later<Clock, T>` needs to mean (a type that only *becomes* `T` after crossing a clock edge, that cannot be read as `T` before that crossing, and that composes across component boundaries via a real type in a signature, per D-013's "critical for agent composition" claim).

The CIRCT lowering side confirms the same finding from a different angle: `crates/strata-circt/src/lib.rs` lowers a `CheckedRegisterUpdate`'s value straight to `%{register_name} = seq.firreg %{next_name} clock ...` (~line 328) — the "next" MLIR value is just the lowered form of the checked value expression, with no intervening modal representation at any IR layer. `reg <- expr` works today, and works soundly for the single-register, non-recursive case, precisely *because* it never needed a `Later` type: a bare register update is a leaf construct (assign a same-cycle-computed value to a next-cycle-visible storage cell), not a *recursive* one. `Later`'s actual job, per D-013's signature, is different and harder: `delay(init, next)` takes `next: Signal<T>` — an expression that is itself allowed to **read the very value being delayed**, closing a feedback loop, which is exactly the shape `reg <- expr` today has no mechanism to check at all (nothing stops, or needs to stop, a plain register update's value expression from being self-referential today, because self-reference through a bare register happens to already be guarded by the register itself at the hardware level — the checker just never had to *prove* that, it got it for free from `seq.firreg`'s semantics). Formalizing `Later` is therefore not "give `reg <- expr` a type it was informally already using" — it is a **new, separate judgment** for a strictly more general construct (arbitrary self-referential `next` expressions, not just a bare storage write), and D-093/D-094's "guarded-feedback vocabulary" language in [17](17-memory-model.md)/[18](18-grade-system.md) was aspirational cross-referencing to the *concept* `later` names, not evidence of literal reusable machinery. This is the same kind of "checked directly, not assumed" finding D-092 §1 modeled for `TypeKind::Array` — except here the answer comes out the other way: **v0 must build a real new judgment, not finish an existing informal one.**

### 3. The v0 decision: a new `delay(init, next)` builtin, one non-nested call per component, no new grammar

**Decision: v0 adds `delay(init, next)` as a recognized builtin call — not new parser grammar, since `ExprKind::Call` already parses arbitrary `path(args)` expressions generically — checked as a new `CheckedExprKind::Delay { init, next }` node (promoting it into checked IR the same way D-092 §6 promoted `Index` from a Ty-only computation), typed `Later<Clock, T>` via a new `TypeKind::Later { domain: Option<String>, inner: Box<TypeRef> }` variant. v0 scopes to exactly one, non-nested `delay` call per component body, its `init` restricted to a same-cycle, non-recursive expression, and its `next` restricted to referencing the `delay`'s own result at most (no mutual feedback between two or more `delay`s).**

**Syntax: nothing new to parse.** `crates/strata-hir/src/lib.rs::ExprKind::Call { callee, turbofish, args }` (line 144) already covers `delay(init_expr, next_expr)` as an ordinary call expression — the same shape `ghost fn` calls, `.wrapping_add(...)`-style method calls, and every other function invocation already use. This is a genuinely different finding from D-094's linear qualifier (which needed a real new binder keyword because nothing linear-shaped existed to parse): **`delay` needs zero `strata-syntax` grammar work.** What's missing is entirely downstream — recognizing the callee name `delay` as a builtin (the same "special-case a known callee path" move `calls_ghost_fn` already makes for `ghost fn`, `crates/strata-check/src/lib.rs` ~line 1908) and giving it a real checked representation instead of falling through to `ArtifactIneligibility::UnsupportedExpression` the way an ordinary unresolved `Call` does today (confirmed: `CheckedExprKind` has no `Call` variant at all — every call expression that isn't specially recognized is checker-invisible past taint-walking).

**Why one non-nested `delay` per component, not the fully general recursive-feedback case D-013's signature admits in principle.** Three considerations, mirroring how D-092 §3 scoped `mem` to one read port/one write port rather than full multi-port:

- **No fixture forces more.** §1 already establishes there is nothing in the corpus to scope against. Absent a forcing example, the responsible default is the smallest slice that still exercises the actual hard part (a self-referential `next` argument that must be checked, not merely accepted) rather than a maximally general recursive-binding-group construct nothing currently needs.
- **This is the shape D-029's own type rule is stated over.** `delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>>` is a single function of one `init`/`next` pair; nothing in D-013/D-029 asks for N mutually-recursive `delay`s resolved as a group (that would be closer to general guarded corecursion — letrec under `▷` — which D-013 explicitly disclaims as out of scope: "full clocked type theory exists only inside proof assistants... no programming language ships it"). Scoping to one non-nested call per component is scoping to exactly what's committed, not inventing a restriction.
- **Mutual/nested feedback is real future work, not a simplicity shortcut.** A design with two registers whose next-values depend on each other (a common shift-register/handshake pattern) still expresses today via two ordinary `reg <- expr;` statements referencing each other's *current* values — that pattern doesn't need `delay` at all, because each individual register update is still a leaf write (§2). `delay`/`Later` earns its keep specifically for the case where the feedback needs to be *typed as a value* — passed to or returned from a function, stored in a signature, checked for causality without opening the body — which D-013's "critical for agent composition" framing says is the whole point. v0's one-call-per-component scope is deliberately the smallest case that already needs a real value-level `Later` type to be sound, without also taking on multi-`delay` interaction, which is genuinely new design space this doc declines to open speculatively (the same posture D-092 §7 took toward true multi-port memories).

### 4. The `Later<Clock, T>` typing judgment

**`Later<Clock, T>` as a type: "not yet, but next cycle in domain `Clock`."** A value of type `Later<'d, T>` cannot be used anywhere a plain `T` is expected — reading it as `T` before crossing the clock edge it names is exactly the unguarded-cycle bug D-013 rejects compositionally. The only two legal operations in v0:

1. **Introduction, via `delay`.** `delay(init: T, next: Signal<T>) -> Later<'d, T>` where `'d` is the clock domain the enclosing component/block is elaborated against (inferred from ambient context, matching how `clock_domain`-scoped bodies already resolve their domain today — no new domain-inference machinery, reusing what `07-compiler-architecture.md`'s domain-inference story already does for `reg`). `init` is checked as an ordinary same-cycle expression of type `T`, with **no self-reference permitted** — `init` may not mention the `delay` call's own result (there is nothing to refer to yet; this is the base case, checked the same way `reg`'s `reset(v)` expression is checked today, an ordinary same-cycle typed expression with no special allowance). `next` is checked as an expression of type `T` **evaluated in a scope where the `delay`'s own result is bound, at type `T` (not `Later<'d, T>`)**, to a synthetic name available only inside `next` — this is the "peel the modality inside the guard" move guarded recursion always needs: syntactically, `next` may refer to the delayed value's *settled* value from the previous cycle, at ordinary type `T`, precisely because by the time `next` next fires, one clock edge has already elapsed. This is the "guardedness" in "guarded feedback": the self-reference is only well-typed because it is provably behind exactly one `Later` step, the same discipline Nakano's `▷`-modality and Guarded Cubical Agda's `later`/`fix` combinator both enforce, specialized to Strata's single unary "next cycle in this domain" case rather than the general ∀κ-indexed clock-variable theory.
2. **Elimination.** A `Later<'d, T>` value may only be consumed by (a) another `delay`'s `next`/`init` position in the *same* domain `'d` (feedback composing with feedback), or (b) crossing into an ordinary `reg <- expr;` update whose target register is itself in domain `'d` — the same "assign it to a `reg` first" discharge pattern D-092 §2's mem-taint diagnostic already tells users to use for one-cycle-delayed `mem` reads, reused here for the identical reason (both are "you're holding a next-cycle value; the legal way to hold onto it across the boundary is a register"). Anywhere else — a component output, a same-cycle comparison, a return value typed `T` — a `Later<'d, T>` value is rejected with a diagnostic naming the judgment (P-9): `"value has type Later<'d, T>; it is not yet valid this cycle — assign it to a register or pass it to another delay's next/init before using it as T"`.

**Checker mechanics.** `CheckedExprKind::Delay { init, next }` is produced by a new small function paralleling `fn index`'s promotion pattern (D-092 §6): resolve the callee path to the `delay` builtin, type-check `init` against the expected `T` (inferred from context — an annotated `let`, or the declared type of whatever the `delay`'s result flows into), open a synthetic scope binding the delayed value's settled type (`T`) for `next`'s type-checking pass, type-check `next` against `T` in that scope, and construct the checked node with a `Ty::Known(TypeKind::Later { domain, inner: Box::new(T) })` result type. `check_type` (`crates/strata-check/src/lib.rs` ~line 5057) gets a `TypeKind::Later { inner, .. } => check_type(inner, ...)` arm, structurally identical to the existing `TypeKind::Stamped { inner, .. } => check_type(inner, ...)`/`TypeKind::Ref(inner) => ...` peeling arms already there.

**Why not reuse `TypeKind::Stamped` for this, the way D-092 reused `TypeKind::Array` for `mem`.** Checked directly rather than assumed, because the reuse move worked for D-092 and is worth trying first here too: `TypeKind::Stamped { domain: Option<String>, inner, event: Option<String> }` already exists and already carries a "domain" field, which looks superficially like exactly what `Later<Clock, T>` needs. It is not a fit. `Stamped` is D-014's epoch-generativity mechanism (`16-syntax.md` §12, §15: "`stamped T` — the one epoch keyword users write," "`Stamped<T,D>` and `Crosses` are elaboration-owned," the unit-epoch normalization rule) — it tags a value with *which reset epoch/domain generation* it belongs to, a nominal-identity concern (D-014, OP-2's adjacent territory) orthogonal to clock-cycle timing. A `Later<Clock, T>` value's whole point is "valid one clock edge from now, in this domain," a *temporal* fact about cycle count, not a *generativity* fact about epoch identity — the same kind of orthogonality D-092 §2 already established for `mem`-read latency ("later" as a timing modality) versus D-014's stamping. Conflating them would let a `stamped` value silently satisfy a `Later` obligation or vice versa, which is exactly the kind of implicit-behavior violation P-1 exists to catch. **v0 needs its own `TypeKind::Later` variant** — structurally small (two fields: an optional domain label, one inner `TypeRef`, mirroring `Stamped`'s shape without adopting its semantics), but a real new variant, not a reuse.

### 5. FIX-ω, resolved: branch (b), structural rejection until ω-promotion ships

D-094 §5/§7 stated the obligation precisely and left it as the binding condition for "whoever implements `delay`/`Later<_,_>` checking next": **"either (a) teach `linear_uses` to recognize a `next`-argument position and ω-promote any linear reference found there... or (b) structurally reject any linear reference inside a `next` argument until (a) is done."** This doc is that implementer. Per D-093 §7 and D-094 §5's shared standing commitment ("must ship atomically with `delay`/`Later` checking, not as a follow-up"), this section makes the choice — **branch (b)** — and specifies it completely enough to implement in the same change as §3/§4's `delay`/`Later` checker work.

**Why (b), not (a).** (a) requires designing what "ω-promoted" concretely *means* for a `LinearBinding`'s exactly-once obligation once a reference to it appears inside `next` — and that design is not as settled as it looks. The corollary D-013 §5 records ("ω-graded periodic capabilities remain usable in feedback") is about capabilities that are **already ω-graded** flowing into feedback cleanly; it says nothing about what happens to a **grade-1** binding's own end-of-scope "must be consumed exactly once" obligation when its only reference is inside a re-executing `next`. Two readings are both defensible and give different answers: (i) a reference inside `next` discharges the obligation once, permanently, regardless of how many cycles later it's "used" again (treating the `delay` call itself as the one consuming event) — but this contradicts ω-promotion's own premise, which is that usage inside a feedback body is *unrestricted*, not single; or (ii) a reference inside `next` never discharges the obligation at all, because "ω" means the count is exempted from the linear tally entirely, which then raises the question of how a linear value is *ever* legally consumed by feedback under this reading, since nothing else counts as consumption either. Resolving this cleanly needs a real answer to "what does 'consumed' mean for a grade-1 binding whose only use is inside a construct that re-executes forever" — exactly the kind of type-system-feature design D-093 §2 and D-094 §2 both explicitly declined to bundle with a narrower, smaller v0 ("inventing both X and its checker simultaneously... is a different (and much larger) decision"). Choosing (a) here would repeat exactly the scope-bundling every prior doc in this series has consistently declined.

(b) has no such gap: it is a pure safety property (nothing that must be consumed exactly once may cross into an unrestrictedly-re-executing context at all, full stop) expressible entirely in terms of `local_linear`'s existing membership, with **no new `UseCount` variant, no change to `linear_uses`'s reconciliation algebra (`combine_linear_uses`, `Select`'s join rule), and no design decision about what "consumed via feedback" means** — because v0 forbids the case outright rather than defining it. It closes the soundness gap OP-7 found (nothing linear can reach a feedback body unvetted, so the "spent once in source, spent once per cycle at runtime" bug is structurally unreachable, the same "unreachable by construction" property D-094 §5 wanted but couldn't get because `delay` didn't exist yet) while leaving (a) as a well-scoped, well-motivated future relaxation once the "what does consumption-via-feedback mean" question gets its own decision.

**The concrete rule, against `linear_uses`'s actual landed shape (`crates/strata-check/src/lib.rs`, commit `3ee33b0`).** `linear_uses(expr, target, name, decl_span)` gets one new match arm for the new `CheckedExprKind::Delay { init, next }` node from §4:

```rust
CheckedExprKind::Delay { init, next } => {
    // `init` is an ordinary same-cycle expression — counted normally,
    // exactly like any other non-branching child (D-094 §4's
    // straight-line sequencing rule applies unchanged).
    let i = self.linear_uses(init, target, name, decl_span);

    // `next` is a re-executing (ω) context per FIX-ω (03 §5). v0 takes
    // D-094 §7 branch (b): linear references inside `next` are
    // structurally forbidden, not counted-and-exempted. This is a
    // membership check against the *whole* `local_linear` map (every
    // still-live linear binding, not just `target`) — every `delay`
    // call site is checked once for this, independent of which linear
    // binding's `linear_uses` walk happens to be in progress.
    self.reject_linear_in_feedback_next(next);

    // `next` never contributes a use of `target` upward: any reference
    // that would have contributed one was already rejected above, so
    // by the time counting matters, `next` is guaranteed linear-clean.
    i
}
```

`reject_linear_in_feedback_next` is a new function, structurally a membership-checking sibling to `mem_tainted`/`ghost_tainted` (a flat structural walk, not a counting one — it has no single `target`, it asks "does any linear-tracked local appear anywhere in this subtree") rather than a sibling to `linear_uses` itself:

```rust
fn reject_linear_in_feedback_next(&mut self, expr: &CheckedExpr) {
    if let CheckedExprKind::Binding(id) = &expr.kind {
        if let Some(binding) = self.local_linear.get(id) {
            self.emit(
                expr.path.clone(),
                expr.span,
                "linear_reference_in_feedback_next",
                "a `linear`-bound value may not be referenced inside a `delay`'s \
                 `next` argument: guarded feedback re-executes every cycle, and \
                 ω-promotion for feedback-body usage (FIX-ω, D-095 §5) is not \
                 implemented in v0 — consume this binding in ordinary \
                 straight-line code before it reaches `delay`",
            );
        }
        return;
    }
    // structural recursion into every child position, same traversal
    // shape as `mem_tainted`/`ghost_tainted` — walks the whole subtree
    // regardless of what it finds, since (unlike `linear_uses`) this is
    // not tracking counts or reconciling branches, only membership.
    for child in expr.children() {
        self.reject_linear_in_feedback_next(child);
    }
}
```

This diagnostic fires **every time** a linear binding is referenced inside `next` — including once per reference if `next` mentions it more than once, matching this checker's existing "fail fast, name every occurrence" posture (`combine_linear_uses`'s double-use diagnostic already does the same). A `delay` call whose `next` argument is entirely free of `local_linear` members type-checks normally; `init`'s ordinary counting is unaffected either way, because `init` is not a re-executing position (§4: it is the base case, evaluated once, at elaboration, exactly like any other same-cycle expression).

**This is a complete resolution, not a deferral.** It is deliberately conservative — it forbids some patterns a fuller (a)-shaped checker might eventually accept (a linear capability legitimately "spent" once by being folded into a feedback accumulator, for instance) — but it is sound, fully specified, and closes the exact gap D-093/D-094 both flagged as non-optional at this boundary. Per those docs' shared standing commitment, this section ships in the same change as `delay`/`Later` checking itself; there is no future doc permitted to defer this a fourth time — either the (a)-relaxation gets its own scoped decision once a concrete pattern needs it (§7's north star), or (b) stands as the permanent answer.

### 6. Pipeline ownership

- **`strata-syntax`.** No changes. `delay(init, next)` parses today as an ordinary `Call` expression (§3) — the first construct in this decision series (D-092/093/094/095) where the syntax layer needs zero new grammar for its v0.
- **`strata-hir`.** No new `StatementKind` (unlike `ghost let`/`linear let`, `delay` is an *expression* builtin, not a statement-shaped binder) — `ExprKind::Call` already lowers correctly; recognition of `delay` as a builtin happens entirely in `strata-check`, the same layering `calls_ghost_fn` already uses (HIR doesn't need to know `delay` is special, only the checker does). One addition: `TypeKind::Later { domain: Option<String>, inner: Box<TypeRef> }` (§4), a peer of `TypeKind::Stamped`.
- **`strata-check`.** The bulk of the work: (a) a `delay`-callee-recognition path structurally paralleling `calls_ghost_fn`'s existing callee-path matching; (b) `CheckedExprKind::Delay { init: Box<CheckedExpr>, next: Box<CheckedExpr> }`, promoted the way `Index` was promoted from a Ty-only computation (D-092 §6); (c) the `Later<'d, T>` typing judgment from §4 — introduction via `delay`, elimination only into another `delay`'s `next`/`init` or a same-domain `reg <- expr;`, rejected everywhere else with a named diagnostic; (d) a `TypeKind::Later` peeling arm in `check_type`; (e) the FIX-ω resolution from §5 — `reject_linear_in_feedback_next` and the one new `linear_uses` match arm, landed in the *same* change as (a)-(d), per §5's non-deferrable commitment.
- **`strata-arch-ir` / `strata-circt`.** A `delay` call that passes checking lowers to **exactly the same `seq.firreg` shape a `reg`/`reg <- expr` pair already produces today** (§2 already established that `reg <- expr` needed no `Later` machinery to lower correctly) — `delay(init, next)` elaborates to a synthesized register (reset value `init`, next-cycle value the lowered form of `next`, `next`'s self-reference resolved to a read of that same register's current value) plus a `Binding::Register` entry, reusing `CheckedRegisterUpdate`'s existing lowering path unchanged. This is worth stating explicitly, mirroring D-093 §6's "no changes at all" framing for grade 0's arch-IR story: **`Later<'d, T>` is a purely compile-time causality-and-timing proof about how a value came to exist; once it's checked sound, the synthesized hardware is indistinguishable from hand-written `reg`/`reg <- expr`.** No new arch-IR node type, no new CIRCT op — `delay`'s entire contribution is at the type-checking layer, exactly as D-013's "critical for agent composition" framing implies (the value it adds is a checked *signature-level* guarantee, not new runtime behavior).

### 7. v0 scope

**In v0:**

- `delay(init, next)` recognized as a builtin call (§3) — no new grammar, a new `CheckedExprKind::Delay` node and a new `TypeKind::Later { domain, inner }` type.
- Exactly one, non-nested `delay` call per component body; `init` restricted to a same-cycle, non-self-referential expression; `next` may refer only to that same `delay`'s own settled value (no mutual feedback between two or more `delay`s).
- The `Later<'d, T>` typing judgment (§4): introduction via `delay`, elimination only into another `delay`'s `next`/`init` (same domain) or an ordinary `reg <- expr;` update (same domain) — rejected everywhere else with a named diagnostic.
- FIX-ω, resolved as branch (b): any `linear`-tracked binding referenced inside a `delay`'s `next` argument is rejected outright, via `reject_linear_in_feedback_next` and one new `linear_uses` match arm, shipped in the same change as the rest of this v0 — not deferred.
- Lowering: a checked `delay` produces exactly the `seq.firreg` shape a hand-written `reg`/`reg <- expr` pair already produces — no new arch-IR node, no new CIRCT op.
- `TypeKind::Later` is a distinct variant from `TypeKind::Stamped` — investigated and rejected as a reuse target (§4): `Stamped` is D-014 epoch-generativity, a different axis from clock-cycle timing.

**Deferred (north star), and why each is safely deferrable:**

- **Multiple/mutual `delay` calls in one component, general guarded corecursion.** No fixture and no committed spec text (§3) asks for more than the unary single-call case; D-013 itself disclaims full clocked type theory / general ∀κ guarded recursion as out of scope. Extending beyond one call is a real future decision once a concrete multi-register feedback pattern forces it, the same "wait for a fixture" discipline D-092 §7 used for multi-port memories.
- **FIX-ω branch (a) — ω-promotion of linear references inside `next`, as a relaxation of §5's branch (b).** Not implementable soundly without first answering what "consumed via feedback" means for a grade-1 binding's end-of-scope obligation (§5's two-reading gap) — a real, separate type-system design question this doc declines to bundle with the smaller, sound v0, the same posture D-093/D-094 both took toward D-039's fuller capability-token design.
- **Multi-clock guarded quantification (∀κ), cross-domain `delay`.** D-013 §5 names this DEFERRED directly; cross-domain feedback stays routed through the existing typed CDC bridge ([04 §7](04-protocols-and-streams.md)), sidestepping the multi-clock modality entirely, exactly as D-013 already commits.
- **A declared combinational-read escape hatch or any interaction with `mem`'s own `later`-modality vocabulary ([17](17-memory-model.md) §2).** `mem`'s registered-read timing and `delay`'s feedback typing are both instances of the same "next cycle" concept at the type-system level (§4 gives `Later<'d,T>` a real definition for the first time), but unifying `mem`'s informal "reuses the guarded-feedback vocabulary" language with this doc's actual `TypeKind::Later` is a genuine follow-on integration this doc does not do — `mem` reads keep their current ad hoc one-cycle-latency taint-based enforcement (D-092 §2/§6) unchanged in v0; retrofitting `mem` reads to be typed `Later<'d, T>` for real is future work, named here so it isn't lost.
- **The post-elaboration whole-graph causality check** D-013 §5 names as a backstop to the signature-level `Later` check. v0 relies on the signature-level check alone (§4); the graph-level backstop is real future robustness work, not required for v0's single-call, non-nested scope to be sound (a lone `delay` call cannot form an unguarded cycle the signature check misses — the backstop earns its keep once multiple `delay`s/components compose, which is itself deferred above).

## North star

FIX-ω branch (a) as a scoped, separately-decided relaxation once a concrete pattern (most likely a capability-token or credit value legitimately "spent" once by folding into a feedback accumulator) forces the "what does consumption-via-feedback mean" question to be answered rather than sidestepped; multi-`delay`/mutual-feedback support and the general guarded-corecursion case; multi-clock guarded quantification (∀κ) once cross-domain feedback needs more than the CDC-bridge escape hatch already provides; unifying `mem`'s informal one-cycle-latency enforcement with this doc's real `TypeKind::Later` judgment so the checker has one timing modality instead of two parallel ad hoc ones; the post-elaboration whole-program causality graph check as a backstop once multi-`delay` composition exists to need one.

## Open problems touching this doc

[OP-7](open-problems.md) (one core calculus) — this doc is the "whoever implements `delay`/`Later<_,_>` checking next" both [18](18-grade-system.md) §7 and [19](19-linearity.md) §5/§7 named as owing FIX-ω atomically with feedback typing; §5 discharges that obligation by choosing and fully specifying branch (b) (structural rejection) rather than deferring a third time. The core-calculus probe's FIX-ω *rule* (ω-promotion) is proven sound at the calculus level (`probes/core-calculus/`); this doc's branch (b) is a strictly more conservative implementation choice than the calculus's own fix, not a contradiction of it — v0 simply doesn't yet build the (a)-shaped checker the calculus's rule would need to be realized as ω-promotion rather than rejection. [OP-8](open-problems.md) (dynamic-latency capabilities) is adjacent — `delay`'s `Later<Clock,T>` is a fixed, statically-known one-cycle delay, the Filament-lineage static-interval case OP-8's committed stance already scopes phase 2 to; nothing in this doc engages OP-8's dynamic-latency question.

````