# Implement grade-1 linearity checking per D-094 · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/commit/3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7)

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

Visibility: public

Requested revision: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Requested commit: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Commit: 3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7

Tree: 67d92740d181e38335e820f4637bd7c0eb833335

Author: versecafe

Committer: versecafe

## Message

```
Implement grade-1 linearity checking per D-094

A new linear let qualifier plus a genuinely new context-splitting
checking discipline — not another taint pass. local_taint/local_grade
are flat HashMap<LocalId, bool>s populated by an OR-shaped walk
(mem_tainted/ghost_tainted); linearity needs a real per-binding use
*count* (Zero/One/Many) with join-point reconciliation, because "used
once in each arm, symmetrically" must collapse to one safe use (only
one arm runs per elaboration) while "used in exactly one arm" must be
rejected as a leak — a distinction a single bit cannot express and
that an OR-taint gets backwards in both directions.

- strata-syntax/strata-hir: `linear let` parses and lowers exactly
  like ghost let (StatementKind::LinearLet, structurally identical to
  the already-landed GhostLet).
- strata-check: local_linear: HashMap<LocalId, LinearBinding> tracks
  Zero/One(Span)/Many(Vec<Span>) per binding. linear_uses walks
  CheckedExprKind counting and reconciling at the one join point the
  checked IR has (Select): symmetric One/One collapses to one safe
  use; asymmetric Zero/One rejects with linear_branch_mismatch naming
  the unconsumed arm; any straight-line double-use rejects with
  linear_double_use (fired once, at the point Many first forms, never
  re-fired as it propagates upward). An end-of-scope sweep rejects
  bindings still Zero at frame exit with linear_never_consumed —
  genuinely new infrastructure, since mem/ghost taint are pure
  rejection-at-sink checks with no "did you finish" obligation.

  A soundness fix beyond the design doc's literal prose, found and
  fixed during implementation: per-statement accumulation is confined
  to locals declared in the same block() frame (frame_linear), never
  an outer frame's locals — without this, a nested block entered while
  checking a Select's arms would double-count uses the owning frame's
  own fold already sees, and a bare `if` (no checked representation at
  all) would let uses inside it silently leak past the missing-else
  obligation. A linear local live across any unchecked/Unsupported
  construct (bare if, match, anything without a CheckedExprKind) is
  conservatively indistinguishable from "never referenced" and
  rejected via the existing never-consumed rule, rather than silently
  accepted.
- No sink-rejection pass, unlike grade 0: a linear value legitimately
  reaching a register/mem/output is normal (D-039's release-as-
  operation), only the count matters, not the destination.
- strata-arch-ir/strata-circt: no changes, confirmed directly — a
  passing linear-checked design's compiled MLIR diffs byte-identical
  (module name aside) against the same design with an ordinary let.

Verified end-to-end via the real CLI: the three bug fixtures each
produce exactly their targeted diagnostic and fail compile; the good
fixture checks clean and its MLIR was diffed directly against its
plain-let twin, confirming zero lowering difference.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

```

## Parents

- [a0828f65437c5a864898323290e15e77383c4a52](https://git.cafe/versecafe/strata/commit/a0828f65437c5a864898323290e15e77383c4a52?format=markdown)

[Source at this commit](https://git.cafe/versecafe/strata/tree/3ee33b0500e1a5c0ada6adc5d8cc9756c2acf5f7?format=markdown)