CP-1a — v4 front-end tokenize/parse + declarative grammar-as-data

src/v4/DECISIONS.md

@@ -39,6 +39,7 @@ through — and moves to Part 1.
 | **L-1** | Verilog/SPICE/English added as **parallel B2-OMNI falsification probes** (T-4.9/4.10/4.11), maximally diverse on purpose. Forks resolved: English = boundary-honesty probe (Shape B emit + fail-closed ingest TestClaim), **not** a language model; SPICE = `extdeps/formats/` (netlist is a data format); Verilog = the IN-B concurrency validation (a needed 6th behavior = C1 escalation, by design caught early) | `TASKS.md` T-4.9/4.10/4.11 + `extdeps/languages/verilog.dag`, `extdeps/formats/spice.dag`, `test/claim/boundary/english_ingest_fail_closed.dag` |
 | **L-3** | **Down-the-stack** B2-OMNI probes added (operator-ratified 2026-05-15, parallel up front): T-4.12 `extdeps/languages/llvm_ir.dag` (SSA IR — generalize down the stack; F ~all-structural), T-4.13 `extdeps/languages/machine_code.dag` (bottom of stack; no cosmetics; disassembly = the extreme fail-closed/no-engine test), T-4.14 `extdeps/languages/ptx.dag` (CUDA SIMT — IN-B bet vs the 5 behaviors). Validates the model across the **full target spectrum** (source→IR→machine code) — concretizes C5-fidelity ("we don't necessarily output a binary; F is model+intent-relative"). **Forks DISSOLVED (cascade-closure, resolves 3250390911; no PROPOSED residue):** neither was a genuine open fork — each is forced by an already-ratified parent, and the alternative *contradicts* a ratified decision. (1) machine_code = ONE model parameterized by an `Isa` — **forced by B2-OMNI** (parameterize-not-enumerate / O(N+M); per-ISA files ARE the N×M trap B2-OMNI forbids). (2) CUDA = model **PTX** — **forced by L-3's own ratified down-the-stack-IR scope**: PTX is the SIMT *IR* layer (the down-the-stack probe T-4.14 exists to test); CUDA-C++ is just another Shape A *source* language already covered by general modeling, so it would not be a down-the-stack probe at all. Per P5 the fork dissolves into already-ratified coordinates, not a new decision | `TASKS.md` T-4.12/4.13/4.14 + `extdeps/languages/{llvm_ir,machine_code,ptx}.dag` |
 | **L-4** | **PROOF-1's prover model lands as `extdeps/languages/lean.dag`** (B-2, side-session 2026-05-15 — operator-ratified). PROOF-1 (#3158, merged) was framed "no new file" and explicitly deferred its prover model to "realized when a lean/coq model lands"; this IS that model. B2-OMNI **structurally requires** a declarative `LanguageModel` file to emit to any target, so PROOF-1's "emit to a lean model" needs exactly this file — adding it is the closed-tree extension operator-ratified here (STRUCTURE.md invariant #1). **ONE prover first — Lean** — scoped to the first theorem class **termination** (A2 structural descent ≈ Lean well-founded recursion / `termination_by`). **Coq is the DEFERRED second-prover falsification probe** ("does the model generalize across provers?" — O(1) per B2-OMNI, added only when a theorem class needs it; same probe posture as L-1/L-3; a future operator-ratified extension, never a silent TODO). Per L-2 the Lean *spec* is modeled, not Mathlib. STRUCTURE count 63→64 .dag | `extdeps/languages/lean.dag` (new) + `STRUCTURE.md` languages enumeration/count + `TASKS.md` PROOF-1/T-15 note; cross-ref DECISIONS PROOF-1 / B2-OMNI / L-2 |
+| **L-5** | **`extdeps/languages/dag.dag` admitted — gunbc's native `.dag` LanguageModel** (operator **Option A**, C1 closed-tree extension 2026-05-16, relay merry-ibex-337). `.dag` is B2-OMNI **language #1** (never hardcoded into the generic `01_tokenize` / `02_parse` walkers); lexical + syntactic authority is declarative **`Node` grammar-data** here, same `extdeps/languages/*` bundle shape as the other Shape-A models. L-2 **spec-first** without an external URL: anchor is repo-owned **`docs/v3-spec.md`** plus the v4 closed tree (`STRUCTURE.md`, `TASKS.md` T-6/T-7). PARSE-1 bodiless-`fn` is a **grammar production in data**, not walker code. STRUCTURE count **64→65** `.dag`. | `extdeps/languages/dag.dag` (new) + `STRUCTURE.md` languages line + total; cross-ref `compiler/01_tokenize.dag` / `compiler/02_parse.dag` + B2-OMNI + PARSE-1 |
 | **QRY-1** | **RETRACTED & reframed (operator-corrected 2026-05-15).** "query = user-defined lens" is wrong: user-vs-kernel is PROVENANCE, not a structural distinction (feedback_naming_is_aliasing) — a decorative name distinguished only by who-authored-it must not exist ("a real distinction, or not exist"). There is NO query concept/noun/subsystem. The REAL axis is **scope/parameterization**, already modeled with no new noun: (1) `SectionRef` (DeclarationScope\|NodeScope) — applying a lens AT a scope; (2) parameterized lens signatures — the **affected-set lens (T-21) `(Dag,Diff)->Witness<ReExecFrontier>` is the archetype**: "the affected set of THIS change" = `affected_set(dag,diff)`, already first-class. Lenses, read at scopes and/or parameterized. No `query.dag`. The B2-OMNI "one read over the Node pivot, all ingested languages" property holds for ANY lens, not a "query" | `lens/application.dag` header + THESIS §1.5 + `lens/affected_set.dag` (T-21) |
 | **PAR-1** | Parallelism (T-13) is a THESIS free consequence, a target-AGNOSTIC lens reporting the independence **FACT** (`Witness<ParallelismMap>`); WHETHER/HOW to realize it is target-DEPENDENT — a cost-derived decision (U1/U2 per-target) at emit(T-11)/eval(T-22), NOT the lens. independence = structural-disjointness ∧ effect-independence (consumes `lens/effect.dag`, B3 — Node-disjoint is necessary not sufficient) ∧ fold-combiner associativity-by-inhabitance (consumes `std/algebra.dag` — parallel-reduce is an algebra fact, not a heuristic). fact ≠ spawn-decision; no annotation, no scheduling heuristic. **User-facing contract:** NOT a "parallelize my code" command (forbidden — engine-shaped from the user's seat); a lens the user READS (same UX as complexity/cost); control = structure not a knob; default introspective with the realize-decision derived+inspectable per target (e.g. honestly "no — CPython GIL"); guarantee via `apply_lens(parallelism, Enforce)` (T-23, uniform opt-in-depth). 4 worked examples embedded | `lens/parallelism.dag` header + `TASKS.md` T-13 |
 | **B1** | One content-addressing scheme: a `std`-level Merkle catamorphism `content_hash : Node -> Hash` over the **canonical-form clause** (a SEPARATE explicit node.dag authority — NOT subsumed by A1, which only covers recursion/axis-closure/generics/termination). `Hash` is an opaque digest (no content accessor, K-1-style). One scheme consumed by T-15/T-20/T-21 + A3 + C5 + structural build/CI artifact caching (a cache key IS `content_hash` of the input subgraph — see `lens/affected_set.dag`). NOT workflow-level | `std/node.dag` — the `Hash` type lands here (re-homed beside `Symbol` by the primitive.dag-decomposition; `Hash` is a content identity, not a scalar); the **B1-CANON block** is the canonical-form clause — operator-DESIGNED & ratified in-header 2026-05-15 (pulled back from worker delegation because every consumer rests on it); the canonical-form clause + `content_hash = merkle_fold ∘ canonical` fold land in `std/node.dag`; T-1 IMPLEMENTS that contract, it does not design it |

src/v4/STRUCTURE.md

@@ -32,8 +32,9 @@ src/v4/
     verification.dag     # TestClaim schema (imported from v3)
     report.dag           # advisory carrier (NOT fail-closed Diagnostic); used by synthesis lens
 
-  extdeps/               # external system contracts (20 files)
+  extdeps/               # external system contracts (21 files)
     languages/           # language models (direction-agnostic — emit AND ingest)
+      dag.dag            # gunbc `.dag` — B2-OMNI language #1 (C1 extension 2026-05-16; relay merry-ibex-337)
       rust.dag
       python.dag
       go.dag
@@ -109,10 +110,12 @@ src/v4/
     fixture/             # canonical input programs
 ```
 
-**Total: 64 .dag files + 5 docs + 5 .gitkeep = 74 files.** (Per invariant
+**Total: 65 .dag files + 5 docs + 5 .gitkeep = 75 files.** (Per invariant
 #1 the enumeration above — not the count — is authoritative; the count is
 a checksum, updated on every operator-ratified file addition/removal.
-−5 .dag 2026-05-15: work-direction meta-layer cut, operator-ratified.)
++1 .dag 2026-05-16: `extdeps/languages/dag.dag` — operator-ratified C1 closed-tree
+extension (Option A, relay merry-ibex-337). −5 .dag 2026-05-15: work-direction
+meta-layer cut, operator-ratified.)
 
 ## Scalar/numeric concept decomposition
 

src/v4/compiler/01_tokenize.dag

@@ -9,22 +9,167 @@
 // A .dag-only character class hardcoded here reintroduces the N×M trap =
 // STOP. See 00_compile.dag B2-OMNI for the pivot.
 //
+// Wave-1 **encoding contract** (grammar-as-data over `Node`, not prose):
+//   **E0 — void lexical fragment**: `LexRules` root is a **type** `Node`
+//   whose connective is **`Conj` with zero children** — exactly zero
+//   lexical productions. The walker recognizes this shape **structurally**
+//   (discriminant + `count(children)==0`), never by `Symbol` spelling.
+//   E0 + empty `String` (`std/text.dag` `string_is_empty`) ⇒ `Produced` empty
+//   `TokenStream`. E0 + non-empty source ⇒ `Rejected` (source not exhausted
+//   — fail-closed; no fabricated tokens).
+//   Further encodings (E1+, keywords, …) land as additional **data**
+//   shapes ratified with the LanguageModel carrier; the walker grows by
+//   `match` on those shapes, not by hardcoding `.dag` surface spellings.
+//
 // Owns:
-//   - TokenStream type (output)
-//   - tokenize: (FreeMonoid<Char>, LexRules) -> Result<TokenStream, Diagnostic>
-//     (LexRules is declarative data from the LanguageModel, not code here)
-//   - character-class predicates (driven by LexRules)
+//   - Token, TokenStream carriers
+//   - LexRules — declarative lexical authority as a finite `Node` tree
+//   - tokenize: (String, file: Symbol, LexRules) -> Outcome<TokenStream>
 //
 // Consumes:
-//   - std/text.dag: Char, String
-//   - std/diagnostic.dag: Diagnostic
-//   - std/witness.dag: Witness<C>
+//   - std/text.dag: String, string_is_empty (= FreeMonoid<Char> boundary;
+//     see std/algebra.dag `free_monoid_is_empty`)
+//   - std/node.dag: Node, NodeKind, TypeNode, ComputationNode, Conj,
+//     Symbol, node_well_formed
+//   - std/collection.dag: List<T>
+//   - std/diagnostic.dag: Diagnostic, Outcome, Locus, Textual, WholeFile,
+//     Correction, ExternalContractUnknown, UserInputBoundary
+//   - extdeps/languages/dag.dag: language-#1 model binds E0 instances (see
+//     `dag_wave1_e0_void_lex`); this file stays encoding-generic.
 //
-// Status: scaffold — fill per TASKS.md T-6
+// Status: Wave-1 — E0 void-lex path is **realized** (`Produced`); richer
+// encodings ⇒ honest `Rejected { … walk_not_realized }` until ratified.
 // Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable
 // contract for the worker. Splitting this file requires explicit operator
 // ratification (substrate extension = stop signal).
 
 
 module v4.compiler.tokenize
 
+
+import v4.std.collection { List }
+import v4.std.diagnostic {
+  Correction,
+  Diagnostic,
+  ExternalContractUnknown,
+  Locus,
+  Outcome,
+  Textual,
+  UserInputBoundary,
+  WholeFile,
+}
+import v4.std.node {
+  ComputationNode,
+  Conj,
+  Node,
+  NodeKind,
+  Symbol,
+  TypeNode,
+  node_well_formed,
+}
+import v4.std.text { Char, String, string_is_empty }
+
+
+// ─────────────────────────────────────────────────────────────────────
+// LexRules — declarative lexical specification as a finite `Node` tree
+// (B2-OMNI grammar-as-data).
+type LexRules = Node
+
+
+// ─────────────────────────────────────────────────────────────────────
+// Token — one classified lexeme in source order.
+type Token {
+  class: Symbol
+  lexeme: String
+  file: Symbol
+  start: Int
+  end: Int
+}
+
+
+// ─────────────────────────────────────────────────────────────────────
+// TokenStream — ordered output of stage 1.
+type TokenStream {
+  tokens: List<Token>
+}
+
+
+// ─────────────────────────────────────────────────────────────────────
+// Reason symbols — owned by this dimension (diagnostic.dag owns schema).
+data tokenize_lexical_walk_not_realized: Symbol = tokenize_lexical_walk_not_realized
+
+data tokenize_lex_rules_not_well_formed: Symbol = tokenize_lex_rules_not_well_formed
+
+data tokenize_lex_e0_source_not_exhausted: Symbol = tokenize_lex_e0_source_not_exhausted
+
+
+fn tokenize_lexical_walk_not_realized_diagnostic(at: Locus) -> Diagnostic {
+  Diagnostic {
+    reason: tokenize_lexical_walk_not_realized,
+    at: at,
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+
+fn tokenize_lex_rules_not_well_formed_diagnostic(at: Locus) -> Diagnostic {
+  Diagnostic {
+    reason: tokenize_lex_rules_not_well_formed,
+    at: at,
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+
+fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic {
+  Diagnostic {
+    reason: tokenize_lex_e0_source_not_exhausted,
+    at: at,
+    correction: Unavailable { reason: UserInputBoundary }
+  }
+}
+
+
+// ─────────────────────────────────────────────────────────────────────
+// lex_rules_node_is_conj_empty_root — structural E0 predicate (Wave-1).
+fn lex_rules_node_is_conj_empty_root(rules: Node) -> Bool {
+  match rules.kind {
+    TypeNode { connective: Conj } => count(rules.children) == 0
+    TypeNode { connective: _ } => false
+    ComputationNode { behavior: _ } => false
+  }
+}
+
+
+// ─────────────────────────────────────────────────────────────────────
+// tokenize — GENERIC lexical ingest (B2-OMNI).
+//
+// Discriminates on **declared** `LexRules` shape; only E0 is realized in
+// Wave-1. No `file` or `text` content branches on language identity.
+fn tokenize(text: String, file: Symbol, rules: LexRules) -> Outcome<TokenStream> {
+  let at = Textual {
+    file: file,
+    extent: WholeFile
+  }
+  if !node_well_formed(n: rules) {
+    Rejected {
+      diagnostic: tokenize_lex_rules_not_well_formed_diagnostic(at: at)
+    }
+  } else if lex_rules_node_is_conj_empty_root(rules: rules) {
+    if string_is_empty(s: text) {
+      Produced {
+        value: TokenStream {
+          tokens: []
+        }
+      }
+    } else {
+      Rejected {
+        diagnostic: tokenize_lex_e0_source_not_exhausted_diagnostic(at: at)
+      }
+    }
+  } else {
+    Rejected {
+      diagnostic: tokenize_lexical_walk_not_realized_diagnostic(at: at)
+    }
+  }
+}