# proposal/18-grade-system.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/5fb00970716bc51374501a76d6d4080f218142c3/proposal/18-grade-system.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 5fb00970716bc51374501a76d6d4080f218142c3 Requested commit: 5fb00970716bc51374501a76d6d4080f218142c3 Commit: 5fb00970716bc51374501a76d6d4080f218142c3 Blob: 9fd57d1cc36e5e8f022296a7f2660556fe5dcbbb Size: 20331 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/5fb00970716bc51374501a76d6d4080f218142c3/proposal/18-grade-system.md?format=markdown) ``` # 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](03-time-and-resources.md). ## 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](open-problems.md)'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` next to the existing `local_taint: HashMap` 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`/`initialize(...)` checking, no `Process` 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](open-problems.md)'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](open-problems.md) (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](open-problems.md) 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. ```