Make keyword completeness decidable, not corpus-witnessed (#51)

The keyword/operator obligation was the one class still checked by the
grammar-derived corpus (leaf coverage). Replace it with a structural,
a-priori discharge: `literalDischarge` confirms every alphabetic literal the
grammar consumes (collectLiterals over every rule + the prec/led tables)
appears, as a scoped word, in some REACHABLE pattern whose scope is a keyword
family — a finite scan of the emitted artifact, no corpus. 248/248 across the
six grammars; non-vacuous (stripping `class` from its patterns reports it
undischarged).

Completeness is now a decidable structural check end to end — token discharge
(census, incl. neuter) + keyword-literal discharge + repository reachability,
952/952 = 100%, no corpus. The leaf-coverage corpus pass is demoted to a
redundant differential cross-check on the soundness axis; `tm-mutation`'s
structural layer now also kills a dropped/neutered keyword corpus-free.

COMPLETENESS.md draws the line correctly: COMPLETENESS (present + reachable +
scoped) is decidable — finite G, finite gen-tm(G), an obligation taxonomy
bounded by TextMate's finite construct kinds, per-token discharge by
structural identity (the flat `match` IS the token's own pattern) — and ∀ G by
structural induction over the finite combinator algebra. SOUNDNESS (do the
present constructs paint correctly on all inputs — wrong-role, pattern
ordering) is the undecidable residual (CFG vs regex-stack-machine over infinite
input). The earlier "a-priori completeness is unavailable" was an
over-concession: that was soundness's wall, mistaken for completeness's.

Author: johnsoncodehk

COMPLETENESS.md

@@ -46,7 +46,10 @@ value of a **closed union**: `RuleExpr` has 15 constructors and `TokenPattern` h
 `aliasScopes`, `expressionRule`, `manifest`). An *obligation* is induced by a
 constructor-occurrence or a config-field-occurrence. So completeness reduces to: **for each
 obligation generator, the generator has a discharging, reachable emission** — three
-mechanically-checkable layers.
+mechanically-checkable layers. Both sides are finite — a finite `G`, a finite `gen-tm(G)`, and an
+obligation taxonomy bounded by TextMate's finite construct kinds — so completeness is a **decidable**
+property per grammar, and holds **∀ G by structural induction** over the finite combinator algebra
+(finitely many cases). It is checked a-priori on the emitted artifact, with no corpus.
 
 ## Layer A — closure: the universe is the algebra, and lowering is total
 
@@ -95,23 +98,28 @@ co-blind):
   region machinery (a `markup` grammar emits no per-token keys), or a region that owns the
   token's delimiter (the JSX `/>` / `</` punctuation). `tokenCensus` classifies every token and
   asserts **zero orphans** — the emitter-completeness proof for tokens.
-- **Keyword literals & Pratt operators** are discharged through the flat backbone (A3) and the
-  prec-table path; the `op`/`prefix`/`postfix` markers carry no literal (they route to
-  `collectLiterals`' default), and an operator's scope comes from the prec-table value, not from
-  a walked marker — so those three constructors being unwalked anywhere is *benign*, confirmed
-  by adversarial review.
+- **Keyword literals & Pratt operators** bear a keyword-scope obligation, **discharged
+  structurally** (`literalDischarge`): every alphabetic literal the grammar consumes (from
+  `collectLiterals` over every rule, plus the prec / led tables) must appear, as a *scoped word*,
+  in some **reachable** pattern whose scope is a keyword family (`keyword.` / `storage.` /
+  `constant.language` / …). This is a finite scan of the emitted artifact — **no corpus** — asking
+  only whether a scoping pattern is *present* (completeness); whether its guard fires correctly is
+  soundness. **248/248** discharged across the six grammars. (The `op`/`prefix`/`postfix` markers
+  carry no literal — they route to `collectLiterals`' default — and an operator's scope comes from
+  the prec-table value, so those three constructors being unwalked is *benign*, confirmed by
+  adversarial review.)
 - **Shapes** (JSX elements, generic/cast angle brackets, regex context, declarations, ternary,
   conditional types, arrow params, contextual operators/modifiers) and **config surfaces**
   (markup, indent, newline, `expressionRule`, `aliasScopes`, `canonicalRepoNames`, `manifest`,
   `inject`) each emit a family of repository entries; that the detectors fire on the *shape*
   rather than on TypeScript-specific names — the detector-completeness requirement — is held by
   `test/agnostic.ts` (synthetic grammars with deliberately non-TS names/delimiters).
 
-The empirical witness that all of the above actually paint is **leaf coverage**: over the
-deterministic grammar-derived corpus (`test/grammar-gen.ts`), every parsed leaf whose
-by-construction role (`buildRoleMap`) is a content/keyword role (keyword / string / number /
-comment) is confirmed to receive a non-root scope. The denominator is fixed (the obligation
-leaves). Result: **2433/2433 across all six grammars.**
+So token, keyword/operator, and reachability discharge are **decidable structural checks on the
+emitted artifact** — the fixed denominator in the ledger, **952/952, no corpus**. A *redundant*
+corpus cross-check (**leaf coverage**: over the deterministic grammar-derived corpus, every parsed
+leaf whose by-construction role is content/keyword gets a non-root scope — **2433/2433**) is kept as
+a differential witness on the soundness axis; it is not the guarantee.
 
 ## Measuring the detector — mutation testing
 
@@ -134,12 +142,19 @@ The honest, measured result:
   artifact's *sequence*, not the grammar's algebra — so no corpus-free structural check reaches it,
   and a scope-preserving reorder slips even the bucket-level differential.
 
-So the claim this document makes is bounded and measured: **every presence / reachability gap is
-caught corpus-free** (mutation-proven, the gate); **wrong-role and ordering gaps are the soundness /
-interaction axis**, reached only by evaluation (the differential, or `test/gap-ledger.ts`), never by
-a grammar-algebraic proof. An a-priori "no gap can hide" over the *whole* gap space is not available
-— ordering and correctness obligations live in the emitted artifact and slide toward regex-vs-CFG
-undecidability — and this document does not claim it.
+The line is precise. **Completeness — every required construct PRESENT + REACHABLE + visually scoped
+— is DECIDABLE**, and decided a-priori with no corpus: a finite grammar `G`, a finite emitted artifact
+`gen-tm(G)`, a finite obligation taxonomy (bounded by TextMate's finite construct kinds), and per-token
+discharge by *structural identity* (the flat `match` **is** `tokenPatternSource(t)`, so no semantic
+regex-matching is needed). ∀ `G` follows by structural induction over the finite combinator algebra.
+What is **undecidable is soundness** — do the present constructs paint *correctly on all inputs*: a
+wrong-role paint, or which of two overlapping patterns *wins* (ordering), is an agreement between a
+CFG-derived role and a regex-stack-machine tokenizer over an infinite input space, which slides into
+regex-vs-CFG undecidability (Oniguruma's `\g<>`/backreferences are non-regular). So this document
+proves completeness and *measures* its detector (mutation testing); soundness it does not claim to
+decide — that is `test/gap-ledger.ts`'s by-construction + corpus axis. The earlier framing that
+"a-priori completeness over the whole gap space is unavailable" was an over-concession: completeness
+is available; it was soundness's wall, mistaken for completeness's.
 
 ## Reachability — root ∪ export surfaces
 
@@ -189,17 +204,17 @@ Auto-generated by `node test/tm-completeness.ts --write`; `--check` fails CI if
 
 <!-- COMPLETENESS-LEDGER:START — auto-generated by `node test/tm-completeness.ts --write`; do not edit by hand. -->
 
-| Grammar | Tokens | Keyword literals | Operators | Repo keys (reachable) | Leaf obligations (painted) |
-|---|---:|---:|---:|---:|---:|
-| typescript | 11/11 | 73 | 53 | 158/158 | 199/199 |
-| javascript | 11/11 | 48 | 51 | 103/103 | 131/131 |
-| typescriptreact | 13/13 | 73 | 53 | 171/171 | 169/169 |
-| javascriptreact | 13/13 | 48 | 51 | 116/116 | 121/121 |
-| html | 7/7 | 0 | 0 | 28/28 | 175/175 |
-| yaml | 19/19 | 0 | 0 | 54/54 | 1638/1638 |
-| **total** | **74/74** | **242** | **208** | **630/630** | **2433/2433** |
-
-**Fixed-denominator completeness: 3137/3137 = 100.00%** (token discharge 74/74 · repository reachability 630/630 · leaf painting 2433/2433). Keyword literals (242) and Pratt operators (208) are discharged through the leaf-painting column. **0 open completeness gaps.**
+| Grammar | Tokens | Keyword literals | Repo keys (reachable) | Leaf cross-check (corpus) |
+|---|---:|---:|---:|---:|
+| typescript | 11/11 | 73/73 | 158/158 | 199/199 |
+| javascript | 11/11 | 51/51 | 103/103 | 131/131 |
+| typescriptreact | 13/13 | 73/73 | 171/171 | 169/169 |
+| javascriptreact | 13/13 | 51/51 | 116/116 | 121/121 |
+| html | 7/7 | 0/0 | 28/28 | 175/175 |
+| yaml | 19/19 | 0/0 | 54/54 | 1638/1638 |
+| **total** | **74/74** | **248/248** | **630/630** | **2433/2433** |
+
+**Decidable completeness: 952/952 = 100.00%** (token discharge 74/74 · keyword-literal discharge 248/248 · repository reachability 630/630) — a structural check on the emitted artifact, no corpus. Leaf cross-check (corpus, redundant): 2433/2433. **0 open completeness gaps.**
 
 <!-- COMPLETENESS-LEDGER:END -->
 

test/tm-completeness.ts

@@ -336,6 +336,61 @@ export function leafCoverage(grammar: CstGrammar, tm: vsctm.IGrammar, opts = GEN
   return { den, painted, uncovered };
 }
 
+// ════════════════════════════════════════════════════════════════════════════
+//  STRUCTURAL literal discharge — DECIDABLE keyword completeness (no corpus)
+//
+//  Every alphabetic literal/operator the grammar consumes bears a keyword-scope obligation.
+//  It is discharged iff it appears, as a SCOPED word, in some REACHABLE pattern whose scope
+//  is a keyword family. This is a finite, structural check on the emitted artifact — the
+//  a-priori (not corpus-witnessed) proof that every keyword is scoped. It asks only whether a
+//  scoping pattern is PRESENT (completeness); whether its guard fires correctly is soundness.
+// ════════════════════════════════════════════════════════════════════════════
+const KEYWORD_FAMILY = /^(keyword|storage|constant\.language|support\.(type|class|function|constant)|variable\.language|entity\.name\.(type|tag)|punctuation\.definition\.keyword)/;
+
+// every reachable pattern NODE (root ∪ export surfaces), the same closure as checkReachability
+function reachableNodes(g: CstGrammar, tmJson: TmGrammarJson): any[] {
+  const scope = tmJson.scopeName ?? `source.${g.name}`;
+  const repo = (tmJson.repository ?? {}) as Record<string, any>;
+  const reached = new Set<string>(); const queue: string[] = []; const out: any[] = [];
+  const visit = (node: any): void => {
+    if (!node || typeof node !== 'object') return;
+    if (Array.isArray(node)) { node.forEach(visit); return; }
+    out.push(node);
+    if (typeof node.include === 'string') { const inc: string = node.include; if (inc.startsWith('#')) queue.push(inc.slice(1)); else if (inc.startsWith(scope + '#')) queue.push(inc.slice(scope.length + 1)); }
+    if (node.patterns) visit(node.patterns);
+    for (const c of ['captures', 'beginCaptures', 'endCaptures', 'whileCaptures']) if (node[c]) for (const v of Object.values(node[c])) visit(v);
+  };
+  visit(tmJson.patterns ?? []);
+  if (g.expressionRule) queue.push('expression');
+  for (const k of Object.keys(g.canonicalRepoNames ?? {})) queue.push(k);
+  while (queue.length) { const k = queue.shift()!; if (reached.has(k)) continue; reached.add(k); if (repo[k]) visit(repo[k]); }
+  return out;
+}
+// the alphabetic words a node SCOPES under a keyword-family scope (lookarounds + `\b`/`\w`-escapes
+// stripped so a word-boundary doesn't fuse with the word, e.g. `\bfrom\b` → `from`, not `bfrom`)
+function scopedAtoms(nodes: any[]): Set<string> {
+  const out = new Set<string>();
+  const keywordScoped = (n: any): boolean => (typeof n.name === 'string' && KEYWORD_FAMILY.test(n.name))
+    || (['captures', 'beginCaptures', 'endCaptures'] as const).some(c => n[c] && Object.values(n[c]).some((cc: any) => typeof cc?.name === 'string' && KEYWORD_FAMILY.test(cc.name)));
+  for (const n of nodes) {
+    if (!keywordScoped(n)) continue;
+    const re = (n.match ?? n.begin ?? '') as string;
+    const cleaned = re.replace(/\(\?<?[=!][^)]*\)/g, ' ').replace(/\\[a-zA-Z]/g, ' ');
+    for (const w of cleaned.match(/[A-Za-z][A-Za-z0-9_$]*/g) ?? []) out.add(w);
+  }
+  return out;
+}
+export interface LiteralDischarge { obl: number; gaps: string[] }
+export function literalDischarge(g: CstGrammar, tmJson: TmGrammarJson): LiteralDischarge {
+  const scoped = scopedAtoms(reachableNodes(g, tmJson));
+  const lits = new Set<string>();
+  for (const r of g.rules) for (const l of collectLiterals(r.body)) if (isKeywordLiteral(l)) lits.add(l.replace(/^@/, ''));
+  for (const p of g.precs) for (const o of p.operators) if (isKeywordLiteral(o.value)) lits.add(o.value);
+  for (const lp of g.ledPrecs ?? []) if (isKeywordLiteral(lp.connector)) lits.add(lp.connector);
+  const gaps = [...lits].filter(l => !scoped.has(l)).sort();
+  return { obl: lits.size, gaps };
+}
+
 // ════════════════════════════════════════════════════════════════════════════
 //  LAYER A (cont.) — the literal-collection backbone is total + drops nothing consumed
 //
@@ -439,21 +494,16 @@ const GRAMMARS: GrammarCfg[] = [
 interface LedgerRow {
   name: string;
   tokenObl: number; tokenDisch: number;        // non-skip tokens, each → a discharge path
-  litObl: number;                              // distinct keyword literals (painted ⇐ leaf coverage)
-  opObl: number;                               // distinct Pratt operators
+  litObl: number; litDisch: number;            // alphabetic keyword literals, each → a reachable keyword-scoped pattern (structural)
   keyObl: number; keyReach: number;            // repository keys, each → reachable
-  leafObl: number; leafPaint: number;          // empirical content/keyword leaves, each → painted
+  leafObl: number; leafPaint: number;          // empirical content/keyword leaves (the corpus cross-check)
 }
-function ledgerRow(name: string, g: CstGrammar, tmJson: TmGrammarJson, r: ReachResult, tc: TokenCensus, cov: CoverageResult): LedgerRow {
-  const lits = new Set<string>();
-  for (const rule of g.rules) for (const l of collectLiterals(rule.body)) if (isKeywordLiteral(l)) lits.add(l);
-  const ops = new Set<string>();
-  for (const p of g.precs) for (const o of p.operators) ops.add(o.value);
-  for (const lp of g.ledPrecs ?? []) ops.add(lp.connector);
+function ledgerRow(name: string, g: CstGrammar, r: ReachResult, tc: TokenCensus, ld: LiteralDischarge, cov: CoverageResult): LedgerRow {
+  const nonSkip = g.tokens.filter(t => !t.flags.includes('skip')).length;
   return {
     name,
-    tokenObl: g.tokens.filter(t => !t.flags.includes('skip')).length, tokenDisch: g.tokens.filter(t => !t.flags.includes('skip')).length - tc.orphans.length,
-    litObl: lits.size, opObl: ops.size,
+    tokenObl: nonSkip, tokenDisch: nonSkip - tc.orphans.length - tc.neutered.length,
+    litObl: ld.obl, litDisch: ld.obl - ld.gaps.length,
     keyObl: r.repoKeys, keyReach: r.repoKeys - r.dead.length,
     leafObl: cov.den, leafPaint: cov.painted,
   };
@@ -464,21 +514,23 @@ function renderLedger(rows: LedgerRow[]): string {
   const L: string[] = [];
   L.push('<!-- COMPLETENESS-LEDGER:START — auto-generated by `node test/tm-completeness.ts --write`; do not edit by hand. -->');
   L.push('');
-  L.push('| Grammar | Tokens | Keyword literals | Operators | Repo keys (reachable) | Leaf obligations (painted) |');
-  L.push('|---|---:|---:|---:|---:|---:|');
-  const sum = { t: 0, td: 0, lit: 0, op: 0, k: 0, kr: 0, lf: 0, lp: 0 };
+  L.push('| Grammar | Tokens | Keyword literals | Repo keys (reachable) | Leaf cross-check (corpus) |');
+  L.push('|---|---:|---:|---:|---:|');
+  const sum = { t: 0, td: 0, lit: 0, ld: 0, k: 0, kr: 0, lf: 0, lp: 0 };
   for (const r of rows) {
-    L.push(`| ${r.name} | ${r.tokenDisch}/${r.tokenObl} | ${r.litObl} | ${r.opObl} | ${r.keyReach}/${r.keyObl} | ${r.leafPaint}/${r.leafObl} |`);
-    sum.t += r.tokenObl; sum.td += r.tokenDisch; sum.lit += r.litObl; sum.op += r.opObl;
+    L.push(`| ${r.name} | ${r.tokenDisch}/${r.tokenObl} | ${r.litDisch}/${r.litObl} | ${r.keyReach}/${r.keyObl} | ${r.leafPaint}/${r.leafObl} |`);
+    sum.t += r.tokenObl; sum.td += r.tokenDisch; sum.lit += r.litObl; sum.ld += r.litDisch;
     sum.k += r.keyObl; sum.kr += r.keyReach; sum.lf += r.leafObl; sum.lp += r.leafPaint;
   }
-  L.push(`| **total** | **${sum.td}/${sum.t}** | **${sum.lit}** | **${sum.op}** | **${sum.kr}/${sum.k}** | **${sum.lp}/${sum.lf}** |`);
+  L.push(`| **total** | **${sum.td}/${sum.t}** | **${sum.ld}/${sum.lit}** | **${sum.kr}/${sum.k}** | **${sum.lp}/${sum.lf}** |`);
   L.push('');
-  // the fixed denominator = every measured obligation (token-discharge + key-reachability + leaf-painting)
-  const den = sum.t + sum.k + sum.lf, num = sum.td + sum.kr + sum.lp;
-  L.push(`**Fixed-denominator completeness: ${num}/${den} = ${(100 * num / den).toFixed(2)}%** ` +
-    `(token discharge ${sum.td}/${sum.t} · repository reachability ${sum.kr}/${sum.k} · leaf painting ${sum.lp}/${sum.lf}). ` +
-    `Keyword literals (${sum.lit}) and Pratt operators (${sum.op}) are discharged through the leaf-painting column. ` +
+  // the DECIDABLE fixed denominator = the structural obligations (token discharge + keyword-literal
+  // discharge + repository reachability), checked a-priori on the emitted artifact, no corpus. The
+  // leaf cross-check is the redundant corpus witness (the soundness-axis dual), reported separately.
+  const den = sum.t + sum.k + sum.lit, num = sum.td + sum.kr + sum.ld;
+  L.push(`**Decidable completeness: ${num}/${den} = ${(100 * num / den).toFixed(2)}%** ` +
+    `(token discharge ${sum.td}/${sum.t} · keyword-literal discharge ${sum.ld}/${sum.lit} · repository reachability ${sum.kr}/${sum.k}) — ` +
+    `a structural check on the emitted artifact, no corpus. Leaf cross-check (corpus, redundant): ${sum.lp}/${sum.lf}. ` +
     `${num === den ? '**0 open completeness gaps.**' : `**${den - num} OPEN GAP(S).**`}`);
   L.push('');
   L.push('<!-- COMPLETENESS-LEDGER:END -->');
@@ -519,14 +571,16 @@ async function main(): Promise<void> {
     const tc = tokenCensus(g, tmJson);
     check(`token-completeness(${cfg.name}): every non-skip token has a discharge path`, tc.orphans.length === 0, `orphans: ${tc.orphans.join(' ')}`);
     check(`token-completeness(${cfg.name}): no flat token is neutered to the bare root scope`, tc.neutered.length === 0, `neutered: ${tc.neutered.join(' ')}`);
+    const ld = literalDischarge(g, tmJson);
+    check(`literal-completeness(${cfg.name}): every keyword literal/operator is in a reachable keyword-scoped pattern`, ld.gaps.length === 0, `undischarged: ${ld.gaps.join(' ')}`);
     const tm = await loadTmFromFiles(cfg.scopeName, { [cfg.scopeName]: cfg.tm, ...(cfg.tmExtra ?? {}) });
     let cov: CoverageResult = { den: 0, painted: 0, uncovered: [] };
     if (tm) cov = leafCoverage(g, tm);
-    check(`coverage(${cfg.name}): every content/keyword obligation leaf is painted`, cov.painted === cov.den,
+    check(`coverage cross-check(${cfg.name}): every content/keyword obligation leaf is painted`, cov.painted === cov.den,
       cov.uncovered.map(u => `"${u.text}"(${u.want})`).slice(0, 8).join(' '));
-    rows.push(ledgerRow(cfg.name, g, tmJson, r, tc, cov));
+    rows.push(ledgerRow(cfg.name, g, r, tc, ld, cov));
     const pct = cov.den ? (100 * cov.painted / cov.den).toFixed(2) : '—';
-    console.log(`  ${cfg.name.padEnd(17)} repo ${String(r.repoKeys).padStart(3)} · dead ${r.dead.length} · tokens ${tc.total - tc.skip - tc.orphans.length}/${tc.total - tc.skip} · leaf-coverage ${cov.painted}/${cov.den} = ${pct}%`);
+    console.log(`  ${cfg.name.padEnd(17)} repo ${String(r.repoKeys).padStart(3)} · dead ${r.dead.length} · tokens ${tc.total - tc.skip - tc.orphans.length}/${tc.total - tc.skip} · keyword-literals ${ld.obl - ld.gaps.length}/${ld.obl} · leaf-xcheck ${cov.painted}/${cov.den}`);
     if (cov.uncovered.length) for (const u of cov.uncovered.slice(0, 6)) console.log(`      UNCOVERED "${u.text}" want ${u.want} ctx …${u.ctx}…`);
   }