# Add D-094: v0 linearity design decision · versecafe/strata

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

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

Visibility: public

Requested revision: a0828f65437c5a864898323290e15e77383c4a52

Requested commit: a0828f65437c5a864898323290e15e77383c4a52

Commit: a0828f65437c5a864898323290e15e77383c4a52

Tree: 95f1359b93037b1e8488493606754fcb16d2dd85

Author: versecafe

Committer: versecafe

## Message

```
Add D-094: v0 linearity design decision

Grade 0 (D-093) had ghost fn/ghost let sitting fully parsed and
inert, a real foothold to finish. Grade 1 has no such foothold —
grep confirms nothing named linear/once/grade exists in the parser,
and the protocol/session/process surface that does parse (a
substantial protocol-declaration feature, ItemKind::Protocol in HIR)
reaches nothing in strata-check and isn't a usable substitute for
D-039's capability-token value anyway.

v0 adds the smallest real new surface: a `linear let` qualifier,
structurally identical to `ghost let`, deliberately not D-039's full
Capability<Resource> type or acquire/release operators (declining the
same scope-multiplication D-093 already declined once). The actual
new infrastructure is the checking discipline itself: local_taint's
flat HashMap<LocalId, bool> OR-taint can't express linearity (an
either-arm-consumed fact needs to be a type error, a both-arms-consumed
fact needs to be accepted as one use, and a flat boolean gets this
backwards). local_linear tracks per-binding Zero/One/Many use counts
with a real join rule at CheckedExprKind::Select, plus an end-of-scope
sweep rejecting never-consumed bindings — genuinely new, since grade-0
and mem-taint are pure rejection-at-sink checks with no "did you
finish" obligation.

match-as-statement and if-without-else stay out of scope because
StatementKind::If/Match don't exist in HIR at all yet — confirmed via
direct inspection, not assumed.

OP-7's disposition is sharper than grade 0's: delay/Later/feedback
have zero code representation anywhere, so the trap isn't excluded by
a checking rule, there's no position in the checker for it to occupy
at all. D-093's FIX-ω commitment is restated as a binding obligation:
whoever implements delay/Later checking must, in the same change,
either ω-promote linear references inside next arguments or reject
them until that promotion ships.

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

```

## Parents

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

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