spec: reserve $ in the Form-A lexer (refs #44)

#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).
2026-05-30 14:41:04 +02:00
parent b151990028
commit c76057008e
1 changed files with 384 additions and 0 deletions
@@ -0,0 +1,384 @@
+# Reserve `$` in the Form-A lexer — Design Spec
+
+**Date:** 2026-05-30
+**Status:** Draft — awaiting user spec review
+**Authors:** orchestrator + Claude
+
+## Goal
+
+Close the latent collision class flagged by issue #44, the follow-up
+to the #43 A2b fix (`55d76ae`) and its raw-buf close audit
+(`b151990`).
+
+`Desugarer::fresh_binder` (`crates/ailang-core/src/desugar.rs:537`)
+mints shadow-rename binders as `<base>$<n>`. Its collision probe
+checks the candidate against `used` (the synthetic-name accumulator)
+and `scope` (in-scope *effective* names). It does **not** see an
+authored binder literally named `<base>$<n>` that is out of scope at
+mint time yet later binds under the same `(def, name)` uniqueness
+key — the exact collapse class #43 closes. The `$`-for-synthetic
+convention (`$mp_N` from `fresh`, `<hint>$lr_N` from `fresh_lifted`,
+`<base>$<n>` from `fresh_binder`) is held by discipline only; nothing
+in the toolchain rejects an authored `$`.
+
+This cycle makes the convention a **lexically enforced invariant**:
+no Form-A *identifier token* may contain `$`. `$` becomes reserved for
+the compiler's synthetic namespace, by construction. That makes
+`fresh_binder`'s probe sound (a `<base>$<n>` candidate can no longer
+alias any authored name, because no authored name can contain `$`) and
+retroactively justifies the whole `fresh` / `fresh_lifted` /
+`fresh_binder` machinery.
+
+The concern is precisely AILang's robustness-against-hallucinations
+identity: latent today (no fixture uses a `$` binder), but a
+hallucinating LLM author emitting Form A could mint a `$` name and
+silently corrupt the uniqueness table.
+
+### Why the lexer is the correct enforcement point
+
+The threat vector is **Form-A source only**. By project design
+(confirmed by the user, 2026-05-30) the client LLM author writes Form
+A exclusively; it is *forbidden* from emitting canonical `.ail.json`
+directly. The only actor that may hand-author `.ail.json` is the
+orchestrator (me), in rare exceptions, as a deliberately
+self-responsible channel. Therefore every authored identifier a
+hallucinating client could produce passes through the Form-A lexer —
+there is no second authoring surface to guard.
+
+This places the invariant exactly at the lexer boundary: **written
+source text contains no `$`; synthetic names come into existence only
+afterwards** (at desugar) and may freely use `$`. That boundary —
+text-in versus AST-internal — coincides with the
+`tokenize` boundary. `$` is a *reserved character*, in the same
+category as `(` and `)`: it has no legitimate use in any authored
+identifier position (verified: zero authored `$` identifiers exist
+anywhere in the checked-in `.ail` corpus; the six `$` occurrences are
+all inside comments, which are stripped before tokenization). A
+reserved character with no positional exceptions belongs in the lexer,
+not in a position-aware AST walker.
+
+This is a deliberate reversal of an earlier draft that placed the
+reject in the check layer. That draft's load-bearing argument — "a
+client could construct `.ail.json` directly, bypassing the lexer" — is
+false under the confirmed authoring contract, so the simpler
+lexer-local reservation is correct. It also requires no AST-position
+machinery: the lexer has no notion of binder-vs-reference, and the
+invariant needs none — `$` is banned in *every* identifier uniformly.
+
+### Note on the `.`/`/` precedent (do not mimic it here)
+
+Def-name reservation of `.` lives in the *check* layer
+(`CheckError::InvalidDefName`, `crates/ailang-check/src/lib.rs:1534`),
+not the lexer — *because* `.` and `/` have legitimate authored uses
+(`std_list.map`, `io/print_str` both lex as single idents) and must be
+allowed in some positions and rejected in others. That positional
+split is exactly what forces a check-layer, AST-aware reject. `$` is
+the opposite: no legitimate use anywhere, so no positional split, so
+the lexer is right. (The issue's premise "lex.rs reserves only `.`" is
+factually wrong on two counts — the lexer reserves no `.` at all, and
+the def-name `.` reject is a check-layer concern — and is corrected
+here.)
+
+### Explicitly out of scope: the `.ail.json` deserialization path
+
+The canonical `.ail.json` deserialization path is **deliberately not
+guarded** by this cycle. Per the authoring contract it is the
+orchestrator's self-responsible channel, not a client-reachable
+surface. Guarding it would defend against the orchestrator's own
+hallucination — a different, lower-priority concern that the user has
+explicitly scoped out. This is a documented non-goal, not an
+oversight; the honesty-rule consequence is that the spec, the
+`fresh_binder` doc-comment, and any future contract text must state
+"authored *Form-A* identifiers cannot contain `$`", never the broader
+"no `Module` can contain a `$` name".
+
+### Explicitly out of scope: the probe-body simplification
+
+Issue #44's design question 4 asks whether the enforced invariant lets
+`fresh_binder` drop a probe check. This cycle **keeps** the probe as
+written; only the now-false doc-comment is corrected. Removing a probe
+branch would couple `fresh_binder`'s correctness to a separable
+property ("`used` is a complete record of every mint") that the fix
+does not require. Out of scope.
+
+## Architecture
+
+### Enforcement: the maximal-run classification arm in `tokenize`
+
+`crates/ailang-surface/src/lex.rs` tokenizes by taking maximal
+non-paren / non-whitespace / non-`;` runs (string literals and
+comments are handled earlier in the scan loop, before a run is formed).
+There is **no** `classify_run` helper today: the classification is
+**inline in the `tokenize` loop** — after the run is sliced
+(`let raw = &input[start..i];`, lex.rs:183) it is classified in place
+into `Tok::Int` / `Tok::Float` / `Tok::Ident` (lex.rs:184-230), and
+`tokenize` returns `Result<Vec<Token>, LexError>`. The reservation is
+enforced as a new guard **immediately after the run is sliced, before
+the `is_int` classification** (i.e. inserted at lex.rs:184): if `raw`
+contains `$`, return `Err(LexError::ReservedDollar { … })`.
+
+The plan may either place the guard inline at that point or extract the
+run-classification into a small helper as part of this iteration;
+inline is the smaller change and the spec's code block (below) is
+written inline. Pre-classification placement (rather than only on the
+ident arm) is chosen so the message is uniform for every `$`-bearing
+run — `x$1`, `$mp_0`, and a malformed `12$3` all report the same
+reserved-character violation, rather than `12$3` masquerading as an
+`InvalidInteger`. The rule expressed is crisp: *a run that becomes a
+token must not contain `$`*.
+
+What is **not** affected, by construction of the scan order:
+
+- **String literals** (`"price: $5"`): handled by the `b'"'` branch in
+  the scan loop *before* a non-delimiter run is ever sliced. `$` inside
+  a string stays legal.
+- **Comments** (`; loop$lr_0 …`): consumed by the `;`-to-EOL branch and
+  never tokenized. `$` inside a comment stays legal. (This is why the
+  six `$`-bearing example files keep parsing.)
+
+### Surfacing: no new wiring
+
+`parse` already converts a `LexError` into `ParseError` via
+`ParseError::Lex(#[from] LexError)`
+(`crates/ailang-surface/src/parse.rs:101-103`; `parse` propagates it at
+`parse.rs:126`, `let toks = tokenize(input)?;`), and the CLI already
+converts a surface parse failure into a diagnostic of code
+`surface-parse-error` whose message is the error's `Display` — the
+`W::SurfaceParse { path, message }` arm in
+`crates/ail/src/main.rs:1339-1347`. So a `$`-bearing source flows:
+`tokenize` → `Err(ReservedDollar)` → `parse` → `ParseError::Lex` →
+`ail check` / `ail parse` print a `surface-parse-error` diagnostic and
+exit non-zero. This channel is pinned green by
+`crates/ail/tests/ct1_check_cli.rs::ail_check_json_on_ail_with_syntax_error_returns_structured_diagnostic`
+(asserts `code == "surface-parse-error"` for a broken `.ail`). No new
+error plumbing, no new `CheckError`, no AST walker, no multi-entry-point
+wiring is required — a strictly smaller change than the check-layer
+alternative.
+
+### Scope: every authored identifier
+
+Because the lexer has no AST, the reservation is uniform across every
+identifier token: top-level def/type/ctor names, fn params, `let` /
+`lam` / `loop` / `let-rec` binders, `match` pattern variables, **and**
+all reference positions and operator-shaped idents. This is a superset
+of "all authored binder names" and is the natural granularity; it
+needs no enumeration of binder kinds and cannot drift out of sync with
+the desugarer's renamable-binder set.
+
+## Concrete code shapes
+
+> The shipped artefact is a *parse-time rejection*. Its empirical
+> evidence is therefore (a) a Form-A snippet that `ail check` must
+> reject after this cycle, and (b) the two exemption cases that must
+> stay accepted forever. The canonical *delivered* code is the
+> in-source lexer test, since a must-fail `.ail` cannot live in
+> `examples/` (see Testing strategy).
+
+### The must-fail source (what a hallucinating author emits)
+
+A fn whose `let` binder is literally `x$1` — the synthetic shape
+`fresh_binder` mints. `$` lexes as an ordinary ident char *today*, so
+this snippet parses and checks clean now; this cycle makes the lexer
+**reject it at parse time**:
+
+```ail
+(module bad
+  (fn main
+    (type (fn-type (params) (ret (con Int))))
+    (params)
+    (body
+      (let x$1 7 x$1))))
+```
+
+After this cycle, `ail check bad.ail` exits non-zero with a
+`surface-parse-error` diagnostic whose message names the reserved `$`
+and its byte offset. (Consequently the spec parse-gate, re-run on this
+block *after* the feature ships, will exit non-zero — expected; the
+block is point-in-time evidence of the accept-today / reject-after
+transition.)
+
+### The two exemptions that must stay accepted
+
+`$` inside a string literal (legitimate data) and inside a comment
+(the existing six example files) must keep lexing clean — forever, not
+just today:
+
+```ail
+(module dollar_ok
+  (fn main
+    ; this comment mentions loop$lr_0 — a synthetic name, must stay legal
+    (type (fn-type (params) (ret (con Str))))
+    (params)
+    (body "price: $5")))
+```
+
+### The delivered lexer test (canonical concrete code)
+
+```rust
+#[test]
+fn dollar_in_ident_is_reserved() {
+    let err = tokenize("x$1").expect_err("`$` in an ident must be a lex error");
+    assert!(
+        matches!(err, LexError::ReservedDollar { ref token, .. } if token == "x$1"),
+        "expected ReservedDollar(\"x$1\"), got {err:?}",
+    );
+}
+
+#[test]
+fn dollar_in_string_literal_is_allowed() {
+    // The `$` lives inside a string; it must NOT trip the reservation.
+    let toks = tokenize(r#""price: $5""#).expect("string-internal `$` is legal");
+    assert!(matches!(toks.as_slice(), [Token { tok: Tok::Str(s), .. }] if s == "price: $5"));
+}
+
+#[test]
+fn dollar_in_comment_is_allowed() {
+    // Comment is stripped before tokenization; the ident `x` survives.
+    let toks = tokenize("x ; mentions loop$lr_0\n").expect("comment `$` is legal");
+    assert!(matches!(toks.as_slice(), [Token { tok: Tok::Ident(s), .. }] if s == "x"));
+}
+```
+
+### North-star slice (what the reservation protects)
+
+The legitimate #43 shadowing idiom — the reservation guarantees no
+authored name can collide with the rename `desugar_module` produces
+(inner `buf` → `buf$1`). This must continue to parse, check, and
+compile clean (no regression), because the `buf$1` mint happens at
+desugar, never re-lexed:
+
+```ail
+(module northstar
+  (fn f
+    (type (fn-type (params) (ret (con Int))))
+    (params)
+    (body
+      (let buf 1
+        (let buf (app + buf 1) buf)))))
+```
+
+### Implementation shape — secondary supporting detail
+
+**(1) New `LexError` variant** — `crates/ailang-surface/src/lex.rs`,
+appended to the enum (after `InvalidEscape`, ~line 75):
+
+```rust
+#[error("reserved character `$` in token {token:?} at byte {start}; \
+         `$` is reserved for compiler-synthetic names")]
+ReservedDollar { token: String, start: usize },
+```
+
+**(2) The reject inline in `tokenize`** — immediately after the run is
+sliced (`let raw = &input[start..i];`, lex.rs:183), before the `is_int`
+classification at lex.rs:184:
+
+```rust
+        let raw = &input[start..i];
+        // raw-buf.#44: `$` is reserved for compiler-synthetic names.
+        if raw.contains('$') {
+            return Err(LexError::ReservedDollar { token: raw.to_string(), start });
+        }
+        // … existing `let first = …; let is_int = …;` classification …
+```
+
+**(3) Doc-comment correction (mandatory, honesty rule)** —
+`crates/ailang-core/src/desugar.rs:528-536`. The current paragraph
+asserts "an authored binder may legally contain `$`" and calls the gap
+"tracked as a follow-up". Both become false. The corrected text states
+the now-enforced invariant: authored **Form-A** identifiers may not
+contain `$` (lexer-enforced in `ailang-surface`), so `fresh_binder`'s
+`<base>$<n>` candidates cannot alias any authored name; the probe
+against `used` + `scope` now guards only against prior synthetic mints
+and in-scope renamed binders. The wording must stay scoped to *Form-A
+authored* names (the `.ail.json` path is intentionally unguarded — see
+out-of-scope above).
+
+## Components
+
+| Component | File | Change |
+|---|---|---|
+| `LexError::ReservedDollar` variant | `crates/ailang-surface/src/lex.rs` | add |
+| `$`-reject inline in `tokenize` (after `let raw = …`, lex.rs:184) | `crates/ailang-surface/src/lex.rs` | add |
+| `fresh_binder` doc-comment | `crates/ailang-core/src/desugar.rs:528-536` | correct |
+| lexer must-fail + exemption tests | `crates/ailang-surface/src/lex.rs` (in-source) | add |
+| surface-level reject test (optional) | `crates/ailang-surface/tests/` | add |
+
+No change to `ailang-check` (no new `CheckError`, no walker, no entry-
+point wiring) and no change to the desugarer logic (doc-comment only).
+
+## Data flow
+
+Authored Form-A text → `tokenize` → **[reject here if any run contains
+`$`]** → `parse` → `Module` → `check` → `desugar_module` (mints
+synthetic `$` names — never re-lexed) → typecheck → codegen.
+
+The reject sits at the earliest possible point and at the exact
+boundary the invariant describes. Everything downstream — including the
+compiler's own `$`-bearing synthetic names — is unaffected, because
+**no pipeline stage ever re-lexes post-desugar output** (verified: the
+only production `tokenize` calls are `parse.rs:126` (`parse`) and
+`parse.rs:149` (`parse_term`), fed only by disk-read source or
+pre-desugar `print` output; `render`, `merge-prose`, and the round-trip
+test all `print` then re-`parse` only *pre-desugar* modules — the
+desugar pass runs after parse and its synthetic names never return to
+`tokenize`).
+
+## Error handling
+
+A single new lexer error, `LexError::ReservedDollar { token, start }`,
+surfaces through the existing `ParseError::Lex` (`parse.rs:103`) →
+`W::SurfaceParse` → `surface-parse-error` diagnostic channel
+(`main.rs:1339-1347`) with no new code. The message names the offending
+token and its byte offset, consistent with the other byte-positioned
+lexer errors (`InvalidInteger`, `UnterminatedString`, …).
+
+## Testing strategy
+
+**Must-fail / exemption (new, in-source in `lex.rs`):**
+
+- `dollar_in_ident_is_reserved` — `tokenize("x$1")` → `ReservedDollar`.
+- `dollar_in_string_literal_is_allowed` — `$` inside `"…"` lexes clean.
+- `dollar_in_comment_is_allowed` — `$` inside a `;` comment is dropped,
+  surrounding idents lex clean.
+- (optional) a `crates/ailang-surface/tests/` integration test feeding
+  a full `(module …)` with a `$` binder through `parse` and asserting
+  `Err(ParseError::Lex(LexError::ReservedDollar { … }))`.
+
+**Hard design constraint — no must-fail `$` fixture in `examples/`.**
+`crates/ailang-surface/tests/round_trip.rs` parses *every*
+`examples/*.ail` with `.expect("parse 1")` and no filter. The existing
+must-fail examples (`eq_float_must_fail.ail`, `raw_buf_reject_str.ail`)
+survive because they *parse* and fail only later at check/type. A `$`
+fixture fails at *parse*, so adding it to `examples/` would panic the
+round-trip test. The reject test therefore lives in-source / in surface
+`tests/`, never as an `examples/` file.
+
+**No-regression (must stay green):**
+
+- The full round-trip corpus — zero authored `$` idents, so every
+  example still parses; the six comment-only `$` files
+  (`local_rec_let_capture.ail` et al.) stay green because comments are
+  stripped pre-tokenization.
+- The 19 existing in-source lexer tests.
+- The #43 shadowing north-star slice parses, checks, and compiles clean
+  (the `buf$1` rename is minted post-parse, never re-lexed).
+
+## Acceptance criteria
+
+1. Any Form-A source containing a `$` in an identifier token (any
+   position — def/type/ctor name, param, `let`/`lam`/`loop`/`let-rec`
+   binder, `match` pattern var, or any reference/operator ident) is
+   rejected by `tokenize` with `LexError::ReservedDollar`, and surfaces
+   through `ail check` / `ail parse` as a `surface-parse-error`
+   diagnostic naming the token and its byte offset.
+2. `$` inside a string literal is accepted unchanged.
+3. `$` inside a comment is accepted unchanged (comment stripped).
+4. The `.ail.json` deserialization path is **not** guarded (documented
+   non-goal); no test asserts it rejects `$`.
+5. The full round-trip corpus and the 19 existing lexer tests stay
+   green; no must-fail `$` fixture is added under `examples/`.
+6. The #43 shadowing idiom still parses, checks, and compiles clean;
+   the `buf$1` rename is unaffected.
+7. `fresh_binder`'s doc-comment no longer claims `$` is legal in
+   authored binders and no longer calls the gap a follow-up; it states
+   the enforced invariant, scoped to *Form-A authored* identifiers.