# Implement grade-0 \(ghost\) erasure checking per D-093 · versecafe/strata

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

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

Visibility: public

Requested revision: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Requested commit: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Commit: 04eb9cf6eeb9719c7af75415695bb35b50afff34

Tree: 0778d04987d419ecbce7d74527b41c991c461153

Author: versecafe

Committer: versecafe

## Message

```
Implement grade-0 (ghost) erasure checking per D-093

Real, enforced grade-0 semantics: a ghost value must never reach a
hardware sink. ghost fn and ghost let already parsed but were fully
discarded downstream (item_name skipped the keyword, GhostStmt fell
to StatementKind::Unsupported) — this finishes that existing dead end
per D-093's posture, rather than adding new surface area.

- strata-hir: ItemHeader.is_ghost (mirrors the unsafe_qual precedent
  from the CDC work), and a real GhostStmt lowering arm producing
  StatementKind::GhostLet instead of Unsupported.
- strata-check: a second one-bit taint pass (local_grade +
  ghost_tainted), structurally identical to mem_tainted/
  reject_if_tainted from the D-092 mem work. Unlike mem's taint, there
  is no legal crossing point for grade 0 — it's rejected unconditionally
  at every sink (register-update value, mem-write value, component
  output) via ghost_value_reaches_hardware_sink. An ordinary let that
  merely forwards a ghost-tainted value also taints and is excluded
  from the lowered artifact, so it can't create a dangling reference to
  a binding that (by design) never entered strata-check's `lets`.
  ghost fn calls are also caught via a syntax-tree walk, since general
  function calls have no checked-IR representation in this checker at
  all yet (a pre-existing gap, not introduced here).
- strata-arch-ir/strata-circt: no changes needed — grade-0 bindings
  are absent from lowered artifacts by construction, confirmed via
  real strata compile output (no trace of a ghost binding surviving
  to MLIR).

Verified end-to-end via the real CLI: ghost-let.strata checks clean
and compiles with no ghost trace in the output MLIR;
ghost-let-bug-reaches-hardware.strata is rejected by both check and
compile with a real diagnostic (correct span, judgment, repair
message).

Honest scope note: ghost fn calls nested inside if/block tail
expressions aren't specially walked by the syntax-tree fallback, since
such expressions already have no checked-artifact representation for
ghost-fn calls either way — falls back to the existing generic
UnsupportedExpression ineligibility rather than the new named
diagnostic. Narrow, pre-existing-shaped gap, not a soundness hole.

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

```

## Parents

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

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