Grade System (Usage Grades, v0)

What the {0, 1, ω} usage-grade semiring (D-024) means operationally, the smallest slice of it that is soundly buildable now, where grades attach, which pipeline stage owns which piece, and why phase modalities (D-011) and typestate-over-linearity (D-026) are explicitly not in this scope. Principles in force: P-1 (no implicit behavior — an erased binder must be provably erased, not erased-by-convention), P-2 (cost visible), P-9 (diagnostics name their judgment). This doc is the Δ/usage half of D-010's stratified judgment for one specific slice; the rest of Δ (temporal capabilities) stays in 03.

Committed design

1. What's actually specified today vs. what exists in code

02-type-system-core.md §3 (D-024) commits to grade algebra {0, 1, ω} — erased / exactly-once / unrestricted — the QTT semiring from Idris 2 (Brady, ECOOP 2021). §2 (D-011) ties grade 0 to two of the four phase modalities: "the erasure grade 0 is the semantics of static and ghost binders." §9 (D-039) makes grade 1 the release-protocol mechanism for hardware resources (must-consume, no destructors). §5 (D-013/FIX-ω, via OP-7's probes/core-calculus/ result) fixes a real unsoundness in how grade 1 interacts with guarded feedback.

None of this has runtime representation. Grepping crates/ for Grade, Usage, Linear, Omega returns nothing. There is no usage-count field on any binding, no grade-checking pass, no promotion rule executed anywhere. This is the same state mem was in before D-092: fully speculative except for one piece of surface syntax that already parses and is silently discarded.

That one piece: ghost. crates/strata-syntax/src/parser.rs already parses ghost fn (fn_item, ~line 705: self.eat_kw("ghost")) and a ghost let name = expr; statement form (stmt_dispatch, ~line 1745, producing a GhostStmt node wrapping a nested LetStmt). Past the parser, both are dead ends:

• crates/strata-hir/src/lib.rs::item_name treats "ghost" purely as a token to skip past when recovering an item's name (~line 1203) — ItemKind (line 189) has no Ghost/erasure variant at all, so ghost fn foo() lowers to an ordinary ItemKind::Function. The fact that it was declared ghost is gone by the time HIR exists.
• lower_block (crates/strata-hir/src/lib.rs, ~line 597) matches NodeKind::LetStmt, RegStmt, RegUpdate, MemStmt, ExprStmt, ReturnStmt explicitly; NodeKind::GhostStmt falls through to the wildcard arm and becomes StatementKind::Unsupported(stmt.kind). A ghost let binding is not merely unchecked — it is not represented in HIR at all, so any body containing one is ineligible for the checked-artifact path today (same "one Unsupported statement poisons the whole component" behavior every other unmodeled statement kind gets).

This is exactly D-026's own pattern (a keyword the task description calls out — "referenced only by a single parser comment with zero actual logic") extended to a second case: ghost parses, and does nothing downstream. It is also the natural v0 landing spot, for the same reason D-092 picked TypeKind::Array over inventing a new Type: don't design new surface syntax when unfinished surface syntax already exists and already names the exact concept (D-011's ghost phase / D-024's grade 0).

2. The v0 decision: grade 0 (erasure) only, no usage-counting

Decision: v0 implements grade 0 — "this binder produces no runtime witness; it is compile-time-only and must not reach a hardware sink" — and stops there. Grade 1 (linear, exactly-once) and general grade ω bookkeeping are north star, not v0.

Three options were on the table:

• (a) Grade-0 only. Smallest possible slice. A binder tagged ghost (grade 0) is checked/inferred to be usable only where erasure is sound (refinement positions, other ghost computation, reify/observe-style metadata) and rejected wherever it would need to produce a runtime signal. No usage counting is needed — erasure is a one-bit fact per binding ("does this reach hardware," yes/no), checked once, not tracked across uses.
• (b) Grade-1 only, narrow. Enforce linearity for one binding class where it obviously matters — the natural candidate is protocol capability tokens (D-039's release protocol: an unconsumed capability is a type error). This is ruled out for v0: protocols are still pure spec. crates/strata-check/src/lib.rs has zero code for Capability<_>, Process<_>, or any protocol type — there is no concrete typed value in the checker today that grade-1 enforcement would attach to. Scoping linear enforcement now would mean inventing both a capability-token type and its checker simultaneously, which is a different (and much larger) decision than "add grades."
• (c) Full {0,1,ω} with usage counting and promotion. Rejected for v0 outright. This needs a genuinely different checking discipline than anything in the checker today (see §4) and reaches directly into OP-7's live soundness concern (§3) before there is any binding class that needs it.

(a) is the only option that is both buildable against the current HIR/checker shape and has a real, motivating, already-half-built target (ghost). It is also self-contained: grade-0 checking is a rejection rule (does an erased value leak into hardware), not a counting discipline, so it does not require the linear-typing infrastructure (b) and (c) would need.

What grade 0 actually buys in v0. A ghost fn or ghost let binding is checked to guarantee: (1) its value can only be produced from other grade-0 (ghost/static) values or refinement/obligation-position uses (already grade 0 per D-024's wave-3 amendment in 02-type-system-core.md §3 — "mentioning a term variable in a refinement bound... neither consumes it nor satisfies its consumption"); (2) it can never be read by a reg/mem write target, a component output, or any other hardware-sink position. This is P-1 made concrete for ghost: today nothing stops a ghost let value (if it were even representable) from silently vanishing into synthesized hardware, because nothing checks it at all.

3. Where grades attach in v0

let bindings only (via ghost let) and whole functions (via ghost fn, where every binder the function introduces and its result are grade 0 by construction — the function itself never emits hardware). Not component parameters, not struct fields, not registers, not mem.

Reasoning, mirroring D-092's "what's forced vs. what's a simplicity choice":

• let/ghost let and ghost fn are the only two forms that already parse. Extending grade-0 checking to them is finishing existing syntax, not adding new surface area — same posture D-092 took toward MemStmt.
• Component/function parameters carrying a grade annotation (ghost params, i.e. "this argument is erased before it reaches the body's hardware output") is a reasonable north-star extension but has no parser support today and is a strictly bigger HIR/check change (Param in crates/strata-hir/src/lib.rs line ~40 has no room for a grade field, and every call site would need grade-aware argument checking). Deferred.
• Registers and mem are never grade-0 candidates — they are runtime storage by definition (D-092's whole point is that a mem binding is the runtime witness), so a "ghost register" is a contradiction, not a variant to support.
• Struct fields carrying per-field grades is real long-term design space (a struct with a mix of hardware and ghost/proof fields) but multiplies the surface (grade becomes part of a type, not just a binder) — out of v0 for the same "don't design a second axis speculatively" reason phase modalities are deferred in §5 below.

4. Pipeline ownership

• strata-syntax. No changes needed for v0's scope. ghost fn and ghost let (GhostStmt) already parse correctly.
• strata-hir. Two additions, both structurally small: (a) ItemKind::Function needs a way to carry ghost-ness — either a new ItemKind::Function { ghost: bool }-shaped change or a sibling is_ghost: bool field on whatever wraps Function headers, so the fact survives past item_name's current skip-and-discard; (b) lower_block needs a GhostStmt => lower_ghost_let(...) arm producing a real StatementKind (a thin wrapper around the existing lower_let path, tagging the resulting local as grade 0) instead of falling into Unsupported. Neither requires new HIR node families — GhostStmt's only child is an ordinary LetStmt.
• strata-check. One new, narrow pass, not a rearchitecture: extend BindingKind (crates/strata-check/src/lib.rs ~line 1518) with a grade tag on Local (or a parallel HashMap<LocalId, Grade> next to the existing local_taint: HashMap<LocalId, bool> field, ~line 1502) and add a second one-bit taint, structurally identical to mem_tainted/reject_if_tainted (~lines 1582, 3748): ghost_tainted(expr, &self.local_grade) walks CheckedExprKind the same way mem_tainted does, and reject_if_erased_at_hardware_sink is called at the same boundary sites reject_if_tainted already is (register-update targets, mem-write values, output values). This is directly reusable infrastructure — grade 0 checking is a propagate-and-reject-at-sink taint, the exact shape the mem/register timing check (§2 of 17-memory-model.md, and D-092's Index from_memory taint) already established. No context-splitting, no per-use counting, no join-point reconciliation is needed for grade 0 alone, because erasure is monotone: once tainted "ghost," a value stays ghost through every pure expression form, and the only question at any sink is a single membership test.
• strata-arch-ir / strata-circt. No new node types. A grade-0 binding that passes checking, by definition, never reaches a Binding::Local/Binding::Register/Binding::Memory lowering — it is compile-time-only, so the correct lowering behavior is absence: ghost bindings simply do not appear in CheckedComponent.lets/registers/output_values (or appear and get filtered before arch-IR construction; either is a valid implementation choice, not a design fork, exactly the same non-fork status D-092 §6 gave the CIRCT lowering-path choice).

Honest gap this exposes. Grade-0 checking needs no new checking discipline — it reuses the taint-propagation shape verbatim. Grade-1 (and full {0,1,ω}) would not: linear usage requires a context-splitting typing discipline (each branch of a conditional must independently account for whether a linear binding was consumed, and the two branches' consumption facts must unify at the join point — "used in the then-arm and not the else-arm" is a type error, not something a single propagated boolean can express). That is genuinely new infrastructure, not an extension of local_taint. This doc does not design it; §6 records it as the named prerequisite for grade 1.

5. Phase modalities (D-011): deferred as a separate decision, not bundled

D-011 commits to four phases (static, hardware, ghost, symbolic) with explicit conversions (reflect, reify, symbolize, observe), and a soundness-load-bearing premise on reflect (elaboration-closedness, found by the wave-2 core-calculus probe). Grades and phases are related — D-011 says grade 0 is the semantics of the static/ghost phases — but they are a different axis: phase is a four-way classification of what kind of thing a value is (elaboration-time constant, physical signal, proof term, solver-controlled symbol), while grade is a usage-count discipline orthogonal to that classification (a hardware-phase value could in principle be used exactly once, unrestricted, or never, independent of it being hardware-phase).

v0 does not implement phase modalities. Concretely out of scope here: static, hardware, and symbolic as checked phases; reflect/reify/symbolize/observe as real conversion operators; the elaboration-closedness premise on reflect. None of these have any parser or HIR support today (the one "static" keyword hit in parser.rs is an unrelated static/solve/prove combinator token, not the phase). Building them is a materially larger effort — four checked classifications and four typed conversions, versus grade 0's single erasure bit — and nothing in the current fixture corpus or checker forces it the way fifo.strata forced mem's port count. This v0 implements only the narrow slice of D-011 that grade 0 already subsumes by the spec's own words ("the erasure grade 0 is the semantics of static and ghost binders"): a ghost-tagged binding behaves like a grade-0/erased value. It does not implement static as a distinct checked phase from ghost, does not implement hardware/symbolic at all, and does not implement any of the four conversion operators. Phase modalities remain their own future decision, scoped and probed on their own terms, not scope-crept into this one because D-011 and D-024 share a section number.

6. Typestate-over-linearity (D-026): blocked on grade 1, deferred whole

D-026 is explicit that typestate is "library-defined states over the core's linearity" — not a language primitive, but a pattern that requires grade-1 consumption to exist as its substrate (state transitions "consume the old-state value linearly," §6 point 2). There is no version of typestate checking buildable independent of linear usage tracking; it is not parallel scope to the grade system, it is downstream of it. Since v0 here stops at grade 0, D-026 is fully deferred, not partially scoped. No Uninitialized<T>/initialize(...) checking, no Process<During, Success, Failure> typing, no state-mismatch diagnostics are in v0. This is a direct consequence of §2's decision, not an independent judgment call.

7. OP-7's ω-promotion concern: not reached by v0, and the fix is already recorded for when it is

OP-7's probe (probes/core-calculus/, wave 2) found a real unsoundness at the grade × later boundary: the naive feedback-typing rule let a grade-1 value be spent once per cycle inside a feedback body, when feedback re-executes every cycle — a bug neither QTT nor guarded recursion alone catches. The fix is already specified, not just flagged: FIX-ω, "usage inside a feedback body is ω-promoted" (03-time-and-resources.md §5) — any binding consumed inside a later-guarded feedback body is treated as grade ω for the purposes of that body's usage check, precisely because re-execution means "used once in the body" really means "used once per cycle, forever."

Disposition for this v0: not reached, and correctly so. FIX-ω is a rule about grade-1 values used inside feedback. v0 has no grade-1 tracking at all — grade 0 values are never legally used to drive a later-guarded feedback body in the first place (§2: a grade-0 value may never reach a hardware sink, and a feedback body's next argument is exactly such a sink). There is no case in this v0's scope where a checker would need to decide whether to promote a linear binding inside feedback, because no binding in this v0's scope is linear. OP-7's promotion concern therefore stays exactly where it is today — moot, because no grade checker exists that could be unsound about it — with one change: this doc names the specific future obligation precisely, instead of leaving it as a general worry. When grade 1 is added (north star, not this v0), FIX-ω is not optional or best-effort: it must ship as part of the same change that adds grade-1 usage-checking inside feedback bodies, per this project's standing enforce-properly-or-don't-ship instruction for foundational judgment work (the same posture D-092 took toward mem timing — permissive/deferred enforcement is not acceptable once the feature is claimed to exist). Concretely, the future grade-1 checker must special-case any binding referenced inside a Later-typed feedback body's next computation and check it under ω, not under 1, before that checker can be considered sound — this is not a "nice to have," it is the literal content of the probe's fix.

8. v0 scope

In v0:

• Grade 0 ("erased," compile-time-only, no runtime witness) as the only tracked grade. No grade 1, no general ω bookkeeping, no usage counting.
• Grades attach to let bindings (ghost let) and whole functions (ghost fn) only — the two forms that already parse. Not parameters, not struct fields, not reg/mem.
• strata-hir: ghost-ness survives past the parser (ItemKind/statement representation carries it; GhostStmt gets a real StatementKind instead of falling to Unsupported).
• strata-check: a second taint pass, structurally identical to the existing mem_tainted/reject_if_tainted mechanism, rejecting a grade-0 value at any hardware-sink boundary (register-update target, mem-write value, component output value).
• strata-arch-ir/strata-circt: no new node types; grade-0 bindings that pass checking are absent from lowered artifacts by construction (they never reach CheckedComponent.lets/registers/output_values).
• OP-7's ω-promotion case is not reached (§7) — explicitly noted as moot-for-now, not silently ignored.

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

• Grade 1 (linear, exactly-once) enforcement. No concrete binding class needs it yet — protocol capability tokens (D-039's natural target) have zero representation in the checker today (§2). Needs genuinely new context-splitting checker infrastructure (§4), not an extension of the grade-0 taint pass.
• General ω-bookkeeping / real usage counting. Only meaningful once grade 1 exists (ω is defined by contrast with "exactly once"); nothing to count against yet.
• FIX-ω / the OP-7 promotion rule as executable code. Specified (§7, and already recorded in 03-time-and-resources.md §5) but not implementable before grade 1 exists. Must land atomically with grade-1-inside-feedback support, not after.
• Phase modalities (D-011) beyond the grade-0/ghost overlap — static as a phase distinct from ghost, hardware, symbolic, and all four conversion operators (reflect/reify/symbolize/observe). Different axis from usage grades (§5); no fixture or checker gap forces it now; scoping it alongside grades would be bundling two independent decisions.
• Typestate-over-linearity (D-026). Structurally requires grade 1 to exist first (§6); not parallel scope.
• Grade annotations on function/component parameters or struct fields. No parser support today; a strictly larger HIR/check change than finishing ghost fn/ghost let.
• Multiplicity polymorphism, dependent multiplicities, menu-based extra semirings (interval grades, security lattices). Already named as north star in 02-type-system-core.md itself; nothing in this v0 changes that assessment.

North star

Grade-1 linear enforcement once a concrete linear binding class exists (most likely gated on protocol capability tokens landing in the checker at all — a prerequisite, not a parallel track); FIX-ω implemented as part of that work; grade annotations widening to parameters and struct fields; phase modalities (static/hardware/symbolic as checked phases, reflect/reify/symbolize/observe as real operators) as their own scoped decision; typestate-over-linearity (D-026) once grade 1 lands; the menu-based extra semirings and dependent-multiplicity tracks D-024 already defers.

Open problems touching this doc

OP-7 (one core calculus) — this v0 does not reach the grade × later promotion case the probe found; §7 records the exact obligation (FIX-ω) that must ship atomically with any future grade-1-inside-feedback support, so the risk is deferred with a named fix in hand, not left as an open question. OP-2 is adjacent (epoch indices vs. signature pollution) but not engaged by grade-0-only scope — epochs are a nominal-generativity concern (D-014), not a usage-grade one.