#44 asks to enforce-or-retract the `$`-in-authored-binder-names
reservation that `fresh_binder` (ailang-core::desugar) relies on for
collision-free shadow-rename mints. This spec chooses enforcement, and
places it in the Form-A lexer rather than the check layer.
The placement is the load-bearing design decision. An earlier draft put
the reject in `pre_desugar_validation` (check layer), justified by "a
client could construct `.ail.json` directly, bypassing the lexer". The
user corrected the threat model: the client LLM author is forbidden from
emitting canonical `.ail.json` — it writes Form A exclusively, and only
the orchestrator hand-authors JSON in rare exceptions. So the entire
hallucinating-client attack surface is Form-A source, which always flows
through `tokenize`. That collapses the design:
- `$` is a reserved character (like `(`/`)`) with no legitimate authored
use in any position — verified: zero authored `$` idents exist in the
checked-in `.ail` corpus; the six `$` occurrences are all in comments.
No positional split, so no AST-aware walker is needed — unlike `.`/`/`,
which DO have legitimate uses (`std_list.map`) and therefore live in
the check layer (`InvalidDefName`). The issue's premise "lex.rs
reserves only `.`" is false on two counts and is corrected in the spec.
- The reject is a single new `LexError::ReservedDollar`, raised inline in
the `tokenize` run-classification arm, surfaced through the existing
`ParseError::Lex` -> `W::SurfaceParse` -> `surface-parse-error` channel.
No new `CheckError`, no AST walker, no multi-entry-point wiring (the
check layer has four entry points, only two of which currently run the
pre-desugar pass — a trap the lexer placement sidesteps entirely).
Documented non-goals (honesty rule): the `.ail.json` deserialization path
stays unguarded (the orchestrator's self-responsible channel, scoped out
by the user); the `fresh_binder` probe-body simplification (issue Q4) is
not bundled — only its now-false doc-comment is corrected.
grounding-check PASS on the final bytes: all six load-bearing assumptions
ratified by green tests; all three Form-A example blocks parse-gate clean
(exit 0 today, by design — the reject is new behaviour). String- and
comment-internal `$` stay legal by scan order; no must-fail `$` fixture
goes under examples/ (the round-trip test parses every fixture there).
Brummel
c76057008e