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 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<During, Success, Failure> (04), never by a destructor. D-026 (typestate) needs the same substrate: "transitions consume the old-state value linearly."

"Once" over what, exactly. 03 §5 (D-013/D-029) pins the subtlety this doc's title flags: guarded feedback is delay : (init: T, next: Signal<T>) → Later<Clock, Signal<T>>, 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 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<Key> ident: Type attach form (session_attach, ~line 1416, the catalog's session<key> operator from 04 §1) 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<Resource>, 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: "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<During, Success, Failure>, 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<LocalId, bool>, 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<LocalId, LinearBinding>, populated when a StatementKind::LinearLet is checked (mirroring where local_taint/local_grade are populated today, ~lines 2177–2198):

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 <span>) is consumed in the 'then' branch but not the 'else' branch at <span> — 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<Clock, T>) 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<LocalId, LinearBinding> 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<Resource> 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<K>, 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<During, Success, Failure> 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 (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'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 is adjacent (epoch indices) but not engaged — nothing in this doc's linear-qualifier scope crosses a reset/epoch domain.