# proposal/19-linearity.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/54efc08232a7296ff1ec4dc6e45d9649c9364dad/proposal/19-linearity.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Requested commit: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Commit: 54efc08232a7296ff1ec4dc6e45d9649c9364dad Blob: ddfccb6013b674d2dcf927ba1e59842abd29ee54 Size: 29212 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/54efc08232a7296ff1ec4dc6e45d9649c9364dad/proposal/19-linearity.md?format=markdown) ```` # Linearity (Usage Grade 1, v0) What grade `1` ("exactly once") means operationally, the smallest slice of it that is soundly buildable now, why it needs new surface syntax that grade `0` didn't, the context-splitting checking discipline that replaces flat taint propagation, and the OP-7 disposition for this slice (decided, not deferred again). Principles in force: P-1 (no implicit behavior), P-2 (cost visible), P-9 (diagnostics name their judgment). This doc is a second slice of the `Δ`/usage half of D-010's stratified judgment; [18](18-grade-system.md) shipped grade `0`, this doc scopes grade `1`. ## Committed design ### 1. What's specified vs. what exists in code, re-verified `02-type-system-core.md` §3 (D-024) commits `{0, 1, ω}`. §9 (D-039) is explicit about what grade `1` is *for*: linearity is the release protocol for hardware resources — "must consume," strictly stronger than Rust's affine "may drop," because hardware release always takes time and can fail (drain a FIFO, close a burst, return a credit). The motivating value shape is a **capability token**: a typed value representing exclusive access to a resource, consumed by an explicit release operation that itself returns a `Process` ([04](04-protocols-and-streams.md)), never by a destructor. D-026 (typestate) needs the same substrate: "transitions consume the old-state value linearly." **"Once" over what, exactly.** [03 §5](03-time-and-resources.md) (D-013/D-029) pins the subtlety this doc's title flags: guarded feedback is `delay : (init: T, next: Signal) → Later>`, and `next` is an ordinary expression **re-evaluated every cycle**. "Used once" inside a straight-line, non-feedback body means once per elaboration of that body — unambiguous. "Used once" inside a `next` argument is ambiguous between "once in the source text" and "once per cycle, forever" — and the wave-2 core-calculus probe ([open-problems.md](open-problems.md) OP-7) found the naive rule picks the wrong one: a grade-1 value spent inside `next` is spent once per cycle at runtime while type-checking as spent once in the source. The fix on record is **FIX-ω**: usage inside a feedback body is ω-promoted for the purposes of that body's check. §5 below re-confirms this doc does not need to execute that fix — but not for the reason grade 0 didn't. **Re-verifying D-093's zero-representation claim (still true, checked directly against current `crates/`).** `grep -n "Capability\|Process<\|protocol\|Protocol" crates/strata-check/src/lib.rs` returns **nothing**. There is no capability-token type, no linear-consumption check, no `Process<_,_,_>` typing anywhere in the checker today. This part of D-093's claim holds unchanged. **What's new since D-093 was written: the protocol surface is not as empty as "zero representation" suggests, but it isn't a foothold for grade 1 either.** `crates/strata-syntax/src/parser.rs` already parses full `protocol Name { ... }` item declarations (`fn protocol`, ~line 1147) with `send`/`recv`/`msg`/`role`/`counter`/`latch`/`repeat`/`if`/`const`/`quiesce`/`invariant` entries — the D-027 user-protocol surface — plus a `session ident: Type` attach form (`session_attach`, ~line 1416, the catalog's `session` operator from [04 §1](04-protocols-and-streams.md)) and a `process { step, done, ok, err }` expression literal (`process_expr`, ~line 2673, D-026's async-transition value shape). `crates/strata-hir/src/lib.rs` gives `protocol` items a real `ItemKind::Protocol` (line 1227) rather than folding them into `ItemKind::Unsupported`. **None of this reaches `strata-check`** — the grep above is definitive. This is exactly D-093's "parses and does nothing downstream" pattern, but for a different, much larger construct than `ghost`: full protocol *declarations*, not a capability-token *value*. A protocol declaration names a trace language; D-039's capability token is a typed value carrying exclusive access to one resource instance. Even if protocols were checked tomorrow, that checking would answer "does this message sequence match the schema," not "was this specific value consumed exactly once" — the two are related (D-039 says capability release *is* a protocol-completion event) but a protocol checker is not a substitute for a linear-usage checker; D-039's token still wouldn't exist as a type. **The capability-token concept specifically still has zero syntax and zero checker representation.** **Confirming there is no linear-shaped sibling to `ghost`.** `grep -n "\"linear\"\|\"once\"\|\"grade\""` across `parser.rs` returns nothing beyond `ghost`'s own `eat_kw("ghost")`. Unlike grade 0, which had `ghost let`/`ghost fn` sitting fully parsed and semantically inert, **grade 1 has no already-parsing binder form to finish.** This is the honest finding the task asked for directly: there is nothing to build the checking discipline on top of without inventing at least a small amount of new surface syntax. §2 makes the call on how small. **A second, independent gap: the checked IR has no branching statement shape at all.** `strata_hir::StatementKind` (line 63) has exactly `Let`, `GhostLet`, `Register`, `RegUpdate`, `Mem`-shaped variants, `Expr`, `Return` — no `If`/`Match` statement variant; `lower_block`'s match falls to `StatementKind::Unsupported` for anything else (confirmed at the same wildcard arm D-093 documented for `GhostStmt` before this doc's change). In `strata-check`, `CheckedExprKind` (line 446) has exactly one branching shape, `Select { condition, then_value, else_value }`, and it is built only from `ExprKind::If { else_expr: Some(_), .. }` — an `if` *expression* with a mandatory `else`, both arms reduced to their block's **tail expression only** via `checked_block_tail` (line 1803), which reads only `block.statements.last()`. `ExprKind::If { else_expr: None, .. }` (an `if` used for side effects, no value) and `ExprKind::MatchExpr` both fall through the same `check_expr_node` match to `_ => None` (line 1799) — **no checked representation at all.** Concretely: today's checker cannot express "this multi-statement branch consumes capability `x`; that multi-statement branch doesn't" for any construct — not because context-splitting logic is missing (it is, and is this doc's subject) but because the *branches themselves* aren't representable as checked multi-statement bodies yet. `match`-as-statement and `if`-without-`else` are both out of reach structurally, independent of grades. ### 2. The v0 decision: a `linear` qualifier on `let`, not a capability-token type **Decision: v0 adds the smallest possible new surface syntax — a `linear` binder qualifier on ordinary `let` (`linear let x = expr;`), structurally identical to `ghost let`'s existing parse/lower shape — and builds grade-1 (exactly-once) checking against it, scoped to straight-line code plus the one ternary branching form (`Select`) that already exists in checked IR. It does not add `Capability`, `acquire`/`release` keywords, or any integration with the protocol/session/process surface named in §1.** Three options were on the table, mirroring D-093 §2's structure: - **(a) Reuse an existing binder form, zero new syntax.** Ruled out — checked directly, not assumed. §1 confirms there is no linear-shaped sibling to `ghost` anywhere in the parser. `GhostStmt`/`ghost let` is erasure-shaped (a fact about a value's phase), not consumption-shaped (a fact about how many times a value is used); reusing it for linearity would conflate two different axes D-024 itself keeps orthogonal to phase (§3 of [02](02-type-system-core.md): "a `hardware`-phase value could in principle be used exactly once, unrestricted, or never, independent of it being `hardware`-phase"). There is genuinely nothing to build on without adding *something*. Unlike D-093, which found a real foothold and built on it, this doc's honest finding is the opposite: no foothold exists. - **(b) The full D-039 capability-token type system, built together with grade-1 checking.** This is D-093 §2 option (b), previously rejected as "inventing both a capability-token type *and* its checker simultaneously, which is a different (and much larger) decision than 'add grades.'" That reasoning still holds and is sharpened by §1's findings: a capability token isn't just a new `Type` variant, it implies acquire/release operations, a release protocol returning `Process`, and (per D-039's last sentence) an `errdefer`-style structural check that every acquired capability has a failure-path disposition in every arm — a second checking discipline on top of the linear-consumption one this doc is scoping. Bundling both is exactly the scope-multiplication D-093 already declined once; declining it again is the more consistent call, not a new one. - **(c) A minimal `linear` qualifier on `let`, decoupled from any resource-acquisition semantics.** This is what's chosen. It tests the actual hard part — context-splitting consumption checking — against the smallest binder shape that can exercise it: an ordinary value, tagged linear, that must be referenced exactly once along every execution path before its scope ends. It says nothing about *what kind* of value warrants linearity (a capability, a credit, an arbitrary computed value) and nothing about acquisition/release as operations. This is real new syntax — cost is not zero, unlike grade 0 — but it is the smallest unit that lets the checking discipline be built and proven against something concrete, the same "decouple the mechanism from the full feature" move D-093 itself gestured at (§4's "this doc does not design [context-splitting]; §6 records it as the named prerequisite") without yet having a place to land it. (c) is chosen because it is the only option that is both real (an actual new checked discipline, not a rehearsal) and small (one new statement-shaped binder, structurally a copy of `GhostStmt`/`GhostLet`, not a type-system feature). It deliberately leaves D-039's capability-token type, acquire/release operators, and the errdefer discipline as a separate, larger, still-future decision — exactly as scoped-out as protocols and typestate were in D-093 §5/§6, for the same reason: no fixture and no landed protocol/capability code forces that larger design yet. ### 3. Where grade 1 attaches in v0 **`let` bindings only** (`linear let`), inside straight-line function/component bodies. Not component parameters, not struct fields, not `reg`/`mem`, not function return values, and — critically, see §5 — not inside a `delay`/feedback `next` argument, because that position has no checker representation to attach to at all. - `linear let` mirrors `GhostLet`'s exact shape at every layer: `strata-syntax` parses it via the same `LetStmt`-wrapping pattern `GhostStmt` uses (a new keyword eaten before the `let`, not a new statement grammar); `strata-hir` gets a new `StatementKind::LinearLet { binding, annotation, initializer }` variant, structurally identical to `GhostLet` (line 77 of `crates/strata-hir/src/lib.rs`); `strata-check` gets a new local-scoped tracking map alongside `local_taint`/`local_grade`. - Unlike grade 0, a grade-1 binding is **not** restricted from hardware sinks — consuming a capability by writing it to a register or driving a component output is the normal case (D-039's whole point: release *is* an operation, often one that touches hardware). v0 therefore does not add a `linear`-specific sink-rejection pass the way grade 0 needed `reject_if_erased_at_hardware_sink`; the check is purely about *count*, not *destination*. - **Not attaching to function/component parameters or return values in v0.** A linear parameter would require the same context-splitting discipline to also reach call sites (did the caller's remaining code still hold an obligation to consume the returned/aliased value), which multiplies the surface the way D-092/D-093 both declined for their respective v0s. `let`-only keeps the discipline's blast radius to one function/component body at a time. - **Not attaching to struct fields**, for the same "second axis on a type, not a binder" reason D-093 §3 deferred it for grade 0. ### 4. The context-splitting checking discipline This is the actual new infrastructure D-093 §4 named as a prerequisite and declined to design. `local_taint`/`local_grade` (`crates/strata-check/src/lib.rs`, ~lines 1506/1514) are `HashMap`, populated by `mem_tainted`/`ghost_tainted` (~lines 3989/4025) — pure structural recursion over `CheckedExprKind` where every branching point (`Select`'s `then_value`/`else_value`) is **OR'd together**: taint from either arm poisons the whole expression, because erasure/mem-taint are monotone facts ("does this value's computation touch a tainted source anywhere"). That shape is unusable for linearity: "referenced in the `then` arm and not the `else` arm" must be a **type error** (leaks the capability if the `else` branch runs), and "referenced once in each arm" must be **fine** (exactly one arm executes at runtime, so exactly one reference actually happens) — a fact a flat boolean cannot represent, and an OR-shaped taint gets exactly backwards (it would silently accept the leak case and correctly, but for the wrong reason, accept the safe case). **Data structure.** A new field on `BodyChecker`, `local_linear: HashMap`, populated when a `StatementKind::LinearLet` is checked (mirroring where `local_taint`/`local_grade` are populated today, ~lines 2177–2198): ```rust struct LinearBinding { span: Span, // declaration site, for diagnostics uses: UseCount, } enum UseCount { Zero, One(Span), // single unconditional use-site Many(Vec), // 2+ uses on some execution path — always an error } ``` **Algorithm.** A new recursive function, `linear_uses(expr: &CheckedExpr, target: LocalId) -> UseCount`, walking `CheckedExprKind` the same way `mem_tainted`/`ghost_tainted` do, but counting and reconciling instead of OR-ing: - `Binding(id)` where `id == target`: `One(expr.span)`. Otherwise `Zero`. - Every non-branching form (`UnaryNot`, `Binary`, `WrappingAdd`, `Index`, and the literal forms): combine children by straight-line sequencing — `Zero + Zero = Zero`, `Zero + One = One`, anything `+ One` when already `One` (or `+ Many`) collapses to `Many` with both spans recorded. This is genuinely new: `mem_tainted`/`ghost_tainted` never needed to distinguish "touched once" from "touched twice" because a single bit can't, and didn't need to — grade 0 is a membership question, not a count. - `Select { condition, then_value, else_value }` is the one join point in v0's scope: compute `c = linear_uses(condition, target)` (unconditional — the condition always evaluates), `t = linear_uses(then_value, target)`, `e = linear_uses(else_value, target)`, independently. **Reconciliation rule:** - If `t == e` (both `Zero`, or both `One` with respectively one span each): the `Select` as a whole contributes exactly `t`'s shape upward (`Zero` stays `Zero`; `One` stays `One`, carrying both candidate spans so a diagnostic can point at either depending on which arm is later found to run in a straight-line double-use) — because exactly one of the two arms executes per elaboration, "used once in both arms, symmetrically" is a genuine single use, not a double use. This is the case the flat-boolean taint pass structurally cannot express and gets wrong in both directions (D-093 §4's exact prediction). - If `t != e` (used in one arm, not the other) **and neither side is `Many`**: reject. Diagnostic (P-9-shaped, names the judgment): `linear binding 'x' (declared at ) is consumed in the 'then' branch but not the 'else' branch at — a linear binding must be consumed on every path or none` (or the mirrored message with arms swapped). This is the leak case D-039 exists to prevent, now caught structurally instead of never being checked at all. - If either side is `Many`: reject regardless of the other side, citing the double-use spans directly — a straight-line double-consumption inside one arm is an error independent of branch symmetry. - Then fold `c + reconcile(t, e)` by the same straight-line sequencing rule as the non-branching case above. - All other expression forms currently reachable from `check_expr_node`'s `_ => None` arm (notably `MatchExpr`, `if`-without-`else`) are **out of scope by construction** in v0: if a linear local's declaration is in scope at a point where the body also contains an unchecked `match`/bare-`if`, v0 conservatively treats any linear local live across such a construct as unable to be proven consumed (the same "poisons the whole component" posture every other `Unsupported` statement already gets elsewhere in this checker) rather than silently ignoring the gap. This is a real limitation, stated as one — see §7's deferred list. Extending `linear_uses` to real multi-statement `if`/`match` branches is blocked on `StatementKind::If`/`StatementKind::Match` existing at all, which is HIR/parser work with no grade-system content, a separate prerequisite this doc does not scope. **Where this hooks into `BodyChecker`.** Two points, both new relative to the mem/ghost passes: 1. **Per-statement accumulation**, alongside where `local_taint`/`local_grade` are updated today (the `Let`/statement-processing loop, ~lines 2177–2298 of `crates/strata-check/src/lib.rs`): for every `linear let`-bound local still tracked in `local_linear`, run `linear_uses` over each subsequent statement's checked expression and fold the result into that local's `UseCount`, emitting the `Many`/branch-mismatch diagnostics from the algorithm above as soon as they're detected (fail fast, same posture as `reject_if_tainted`). 2. **End-of-scope sweep** — genuinely new, nothing today needs it. At the close of the block/function that owns a `linear let` binding, every entry still in `local_linear` is checked: `Zero` → reject ("linear binding `x` declared at is never consumed"); `One` → accept, drop from tracking; `Many` → already rejected at accumulation time. Grade 0 and mem-taint never needed an end-of-scope pass because they are pure rejection-at-sink checks with no "did you finish" obligation; grade 1's entire point is that non-consumption is itself the error, which only a scope-exit sweep can catch. ### 5. OP-7's ω-promotion trap: not reached, and not by scope choice this time — by omission at a lower layer **Disposition: structurally unreachable in v0, and unlike grade 0's version of this same disposition, that unreachability isn't a property of the checking rule, it's a fact about what's implemented at all.** `grep -n "\"delay\"\|Later\|feedback" crates/strata-check/src/lib.rs crates/strata-hir/src/lib.rs` returns **nothing**. Guarded feedback (D-013's `delay`, D-029's `Later`) has zero code representation anywhere in this codebase today — not partially checked, not parsed-and-discarded the way `ghost`/protocols are, but entirely absent as a recognized construct. There is no `next`-argument position for `strata-check` to identify, because there is no `delay` call, no `Later` type, no feedback-body notion at all in the checker. This means the OP-7 trap cannot be reached by v0's `linear_uses` pass for a reason stronger than D-093 §7's grade-0 argument. Grade 0's disposition rested on a checking-rule fact ("a grade-0 value may never reach a hardware sink, and feedback's `next` argument is exactly such a sink" — the rule itself excludes the case). Grade 1's disposition here rests on an infrastructure fact: **the position the trap lives in does not exist in the checker to be excluded from or included in.** If `delay`/`Later` were implemented tomorrow without this doc's `linear_uses` pass being updated, a linear local referenced inside a `next` argument would simply be checked by the ordinary straight-line/`Select` rules above — counted once, accepted — which **would silently reproduce the exact bug OP-7 found** (spent once in source text, spent once per cycle at runtime), because nothing in §4's algorithm has any notion of "this expression is inside a re-executing context." **This is not a second punt on grade 1 as a whole — v0 ships real, checked, exactly-once enforcement for straight-line and single-`Select`-branch code today. It is a narrow, explicitly-named punt on exactly one interaction: grade-1-inside-feedback.** Per D-093 §7's standing commitment ("FIX-ω... must ship atomically with any future grade-1-inside-feedback support, not as a follow-up"), that commitment is restated here, sharpened to name the actual future obligation precisely: **whoever implements `delay`/`Later<_,_>` checking must, in the same change, either (a) teach `linear_uses` to recognize a `next`-argument position and ω-promote any linear reference found there (treat it as unconstrained by the exactly-once count for that specific usage, per FIX-ω's rule), or (b) structurally reject any linear reference inside a `next` argument until (a) is done.** Shipping `delay`/`Later` checking with `linear_uses` left as this doc specifies it — silently applying straight-line counting inside feedback — is not a permissible partial state; it is the exact soundness bug the wave-2 core-calculus probe found and fixed on paper. This is now the second time this project has written down that FIX-ω is non-optional at that boundary; there will not be a third deferral available once feedback typing lands. ### 6. Pipeline ownership - **`strata-syntax`.** One addition: a `linear` keyword recognized in `let`-statement position, parsed the same way `ghost`'s `eat_kw("ghost")` gates `GhostStmt` (a token eaten before dispatching to the ordinary `LetStmt` production, producing a `LinearStmt` wrapper node — structurally, not semantically, new). - **`strata-hir`.** One addition: `StatementKind::LinearLet { binding, annotation, initializer }`, added next to `GhostLet` (`crates/strata-hir/src/lib.rs` line 77), and a `NodeKind::LinearStmt => ...` arm in `lower_block` producing it (paralleling the `GhostStmt` arm at line 635) instead of falling to `Unsupported`. - **`strata-check`.** The bulk of the new work, all described in §4: a `local_linear: HashMap` field on `BodyChecker`; the `linear_uses` recursive counting-and-reconciliation function (a new, genuinely different shape from `mem_tainted`/`ghost_tainted`, not a copy); per-statement accumulation hooked in alongside the existing taint-population loop; an end-of-scope sweep (new — nothing today has one) emitting "never consumed" diagnostics; branch-mismatch and double-use diagnostics fired during accumulation. No sink-rejection pass is needed (§3) — grade 1 doesn't restrict *where* a value may be used, only *how many times*. - **`strata-arch-ir` / `strata-circt`.** **No changes at all**, and this is worth stating explicitly because it's the opposite of grade 0's story: a grade-0 binding that passes checking is *absent* from lowered artifacts by construction (D-093 §4); a grade-1 binding that passes checking is behaviorally and structurally **identical to an ordinary `let`** once elaboration reaches arch-ir — `linear` is a purely compile-time bookkeeping fact about *usage shape*, with zero runtime representation and zero lowering difference. `linear let x = f();` lowers exactly like `let x = f();` would. ### 7. v0 scope **In v0:** - A new `linear` qualifier on `let` bindings only (`linear let x = expr;`), parsed and lowered structurally identically to `ghost let`. - Exactly-once consumption checking over straight-line statement sequences and the one existing ternary branching form (`CheckedExprKind::Select`, i.e. `if`-`else` used as a value), via the `local_linear`/`linear_uses` mechanism in §4. - A real join-point reconciliation rule at `Select`: consumed in both arms symmetrically is accepted as one use; consumed in exactly one arm is rejected with a diagnostic naming which arm leaves it unconsumed; any straight-line double-use is rejected regardless of branching. - An end-of-scope sweep rejecting a `linear let` binding that reaches the end of its owning block/function still unconsumed. - No sink restrictions (unlike grade 0) — a linear value may be consumed by reaching a register/mem/output write; only the count is checked. - No new arch-IR/CIRCT node — a checked linear binding lowers exactly like an ordinary `let`. - OP-7's ω-promotion case is not reached, because `delay`/`Later` have zero checker representation to reach (§5) — explicitly noted as an active future obligation with a two-branch resolution spelled out, not silently ignored. **Deferred (north star), and why each is safely deferrable:** - **`match`-as-statement and `if`-without-`else` branch reconciliation.** Blocked on `StatementKind::If`/`StatementKind::Match` existing at all — currently `Unsupported` regardless of grades (§1). This is HIR/parser infrastructure, not a grade-system decision; extending `linear_uses` to real multi-statement divergent blocks is straightforward once that lands (the reconciliation rule in §4 generalizes directly to N-armed matches — "consumed identically across every reachable arm, or rejected naming the odd arm out"), but building it now would mean designing and shipping unused general branch-statement lowering as a side effect of this doc, which is exactly the scope-creep this project's other decisions have consistently declined. - **Grade-1-inside-feedback (the OP-7 boundary) and FIX-ω as executable code.** Not implementable before `delay`/`Later<_,_>` typing exists at all (§5). The resolution shape (ω-promote references inside `next`, or reject them until promotion ships) is specified; it must land atomically with feedback typing, per D-093 §7's standing commitment, restated and sharpened here. - **D-039's capability-token type** (`Capability` or equivalent), acquire/release operators, and the `errdefer`-style structural discharge-obligation check. Rejected for v0 for the same reason D-093 §2 rejected it: a materially larger, separate decision bundling a new type-system feature with the checking discipline. This doc's `linear` qualifier is deliberately not that type — it is the substrate the discipline was proven against, not the resource-management feature D-039 ultimately wants. - **Linear parameters, return values, and struct fields.** No parser support, and each multiplies the surface the context-splitting discipline has to reason about (cross-call obligations, cross-type-position grades) well beyond what `let`-only needs (§3). - **Integration with the protocol/session/process surface** (`protocol`, `session`, `process{...}` — all confirmed parsing in §1, all confirmed absent from `strata-check`). None of D-027's protocol machinery is checked today; wiring linear capability release into protocol completion (D-039's stated eventual design) is downstream of both this doc's discipline *and* a protocol-checking decision this project hasn't made yet. - **Typestate-over-linearity (D-026).** Still structurally downstream, per D-093 §6 — now one layer closer (a real linear-consumption check exists) but D-026 additionally needs state-indexed types and `Process` typing, neither of which this doc adds. - **General `ω`-bookkeeping.** Still only meaningful in contrast to a real "exactly once" — this doc supplies that for the `linear`-qualifier substrate, but `ω` as a third, explicit, user-facing grade (as opposed to "everything not `ghost`/`linear` is implicitly unrestricted by omission, which is v0's de facto default") remains unbuilt. ## North star The D-039 capability-token type and its acquire/release/`errdefer` discipline, built on top of this doc's consumption-counting mechanism once a concrete use case forces it (most likely once the protocol catalog or a component needing explicit resource release lands); general multi-armed branch reconciliation once `if`/`match`-as-statement exist as checked constructs at all; FIX-ω as executable code, shipped atomically with `delay`/`Later<_,_>` checking; linear parameters and struct fields; the eventual wiring of capability release into protocol-completion events D-039 names as the long-run design; typestate-over-linearity (D-026) once both this doc and the protocol/state-indexed-type work land. ## Open problems touching this doc [OP-7](open-problems.md) (one core calculus) — this v0 cannot reach the grade × `later` promotion case because `delay`/`Later` have no checker representation at all (§5), which is a stronger form of "not reached" than [18](18-grade-system.md)'s grade-0 disposition; the exact two-branch resolution (ω-promote or reject-until-promoted) is specified here as the binding obligation for whoever implements feedback typing next. [OP-2](open-problems.md) is adjacent (epoch indices) but not engaged — nothing in this doc's `linear`-qualifier scope crosses a reset/epoch domain. ````