diff --git a/dag/gunbc/plans/cardinality_refinement.dag b/dag/gunbc/plans/cardinality_refinement.dag index d5dc1a1a1f3..0903236a5a3 100644 --- a/dag/gunbc/plans/cardinality_refinement.dag +++ b/dag/gunbc/plans/cardinality_refinement.dag @@ -7,31 +7,30 @@ import gunbc.plans.md_helpers { h2, p, li, ul, ol } fn cardinality_refinement_body() -> List { [ p(text: "**Status:** scoping (Feature-1 from the byte-grounding thread). **DESIGN.md + carriers are authority** (§6 no parallel ledger); each item dissolves into a wired parser/checker change + a green witness when it lands."), - p(text: "**Verified against the live tree 2026-06-22.** Line numbers are receipts; re-check before acting."), + p(text: "**Verified against the live tree 2026-07-31.** Symbols, not line positions, are receipts; re-check the cited declarations before acting."), h2(text: "0. Thesis — cardinality is ONE axis, and it is the *decidable* refinement fragment"), p(text: "\"Is it empty\", \"does it have N\", \"did `Int64` overflow\" are the same question — a **cardinality constraint** — answered today by scattered manual `if list_length(..) == 0` / `count` / bound checks. Model cardinality as a refinement **axis** and two things fall out:"), ol(items: [ - li(text: "**Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`admits: fn(B) -> Bool`, `refinement.dag:34`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it."), + li(text: "**Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`v2.std.refinement` `Validation.admits: fn(B) -> Bool`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it."), li(text: "**Fold-propagation (the payoff).** A catamorphism that carries the cardinality means folding a `List` yields its length, adding two bounded `Int64` yields the combined bound (and **overflow is a typed `Rejected`, not a silent wrap**). \"When we fold, it's handled automatically\" — the empty/count/width checks stop being hand-written."), ]), h2(text: "1. What is ALREADY built (this is wiring, not greenfield)"), ul(items: [ - li(text: "**Value-level refinement substrate — `v2.std.refinement`:** `Validation \{ reason, admits: fn(B)->Bool \}`, `Refined \{ base \}`, and `refine(base, by, at) -> Outcome>` (`:74`) which checks `admits(base)` and returns `Accepted\{Refined\}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements."), - li(text: "**Its own documented gaps:** `🟡 feature:refinement-opaque-carrier / T-25-tail` (`:65`) — bare `Refined \{ base \}` can still bypass `refine`; construction is **not compiler-enforced** yet."), - li(text: "**The phantom-width gap — `std.machine_constraints`:** `type MachineWidth` (`:47`) is a phantom; its TRACKED PARAMETER GAP (`:34-46`) names the exact trigger: *\"substrate grammar for bounded phantom parameters tying `bits` to `Nat`, or a non-phantom `MachineWidth` indexed by an explicit `Nat` carrier.\"* No reflection of `N` to a value."), - li(text: "**The structural carriers exist, unchecked — `std.bit`:** `Byte \{ bits: List \}` (`bit.dag:25`), header concedes *\"cardinality is not enforced … no lowered field refinement, type-alias `where` is skipped in the handwritten parser.\"*"), - li(text: "**A waiting consumer — `std.measure`:** `Refined, predicate>` is explicitly **deferred** (`measure.dag:8,245`), waiting on exactly this."), + li(text: "**Value-level refinement substrate — `v2.std.refinement`:** `Validation`, `Refined`, and `refine` check `Validation.admits` and return `Accepted\{Refined\}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements."), + li(text: "**The carrier has not consumed the existing construction wall:** `v2.std.refinement` `Refined` exposes its `base` field and is not marked `sole_constructor`. The compiler already refuses cross-module construction of `sole_constructor` records through `v1.compiler.infer` `type_has_sole_constructor` / `SoleConstructorViolation`; per DESIGN §4b, its completeness for generic refinement carriers, every construction form, and compiler-module exemptions is **unverified**, not absent."), + li(text: "**The phantom-width gap — `std.machine_constraints` `MachineWidth`:** the declaration has a type parameter but no value carrier. No reflection of `N` to a value exists."), + li(text: "**The structural carrier exists, unchecked — `std.bit` `Byte`:** its `bits: List` field carries no cardinality refinement."), ]), h2(text: "2. The gap, decomposed (each piece → a real surface)"), ul(items: [ - li(text: "[ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Parser: extend the type-RHS path (`parse_type_rhs_after_eq`, named in `machine_constraints.dag:109`) and the record-field path to accept `where `; lex the `where` keyword. Normalize: at the `^dag_surface_type_alias_rhs` hook (`03_normalize.dag:90`) lower `where P` into a `Validation` + a **refined-construction obligation** on the type. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression."), - li(text: "[ ] **P2 — compiler-enforced construction (closes T-25-tail).** Checker: at a construction site of a refined type, require the obligation discharged — bare `Byte \{ bits: … \}` outside the sanctioned `refine`/smart-constructor is a located `Rejected`, never silent. This is what turns \"documented intent\" into \"illegal-state-unwritable.\""), - li(text: "[ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length` (`== N`), `NonEmpty` (`≥ 1`), `Bounded`, `Width` (the `MachineWidth` bound). All are linear-arithmetic over `list_length` (`types.dag:233`) / magnitude — decidable. `Byte = \{ bits: List \} where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.**"), + li(text: "[ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Extend `v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr` and the record-field grammar to accept `where `. Register the emitted surface form through `v2.std.compilers.sugar` and lower it through `v2.compiler.normalize` `normalize_sugar_key_optional` into a `Validation` + a **refined-construction obligation**. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression."), + li(text: "[ ] **P2 — audit and consume the existing construction wall (closes T-25-tail).** First run discriminating positive/negative probes for `sole_constructor` on generic `Refined`, every record-construction form, and the compiler-module exemptions named by DESIGN §4b. If that audit is complete, mark the canonical refinement carrier and route sanctioned construction through `refine`/its smart constructor; if a probe escapes, extend the existing wall at that measured gap rather than minting a parallel checker. The required outcome is that bare refined construction outside the sanctioned factory produces a located `SoleConstructorViolation`, never silent acceptance."), + li(text: "[ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length` (`== N`), `NonEmpty` (`≥ 1`), `Bounded`, `Width` (the `MachineWidth` bound). All are linear-arithmetic over `std.types` `list_length` / magnitude — decidable. `Byte = \{ bits: List \} where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.**"), li(text: "[ ] **P4 — fold-propagation (the novel, high-value piece).** Extend the catamorphism (`fold_node` / the reduce) so a cardinality fact is COMPUTED through a fold: `Cons/Empty` over a list yields its length; combining two `Bounded` magnitudes yields the combined bound, and a bound exceeding the `Width` is a typed overflow `Rejected`. Connect to the existing cost-through-folds algebra (`induction.dag` PolyCost/exponents) — cardinality is the same shape (a count tracked through a catamorphism) as the cost lens already computes."), - li(text: "[ ] **P5 (stretch) — type-level-Nat reflection.** Reflect `MachineWidth`'s `N` to a value (the phantom→value bridge named in `machine_constraints.dag:43-46`), so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal."), + li(text: "[ ] **P5 (stretch) — type-level-Nat reflection.** Add the value bridge absent from `std.machine_constraints` `MachineWidth`, so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal."), ]), h2(text: "3. Where it plugs into the pipeline"), - p(text: "`tokenize` (lex `where`) → `parse` (`parse_type_rhs_after_eq`: parse the cardinality pred, attach to the type-decl `Node`) → `normalize` (`dag_surface_type_alias_rhs`: desugar to `Validation` + the construction obligation) → `infer` (`04_infer`: discharge the obligation at construction sites — the decidable cardinality check — and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time)."), + p(text: "`tokenize` (lex `where`) → `parse` (`v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr`: attach the cardinality predicate to an emitted surface node) → `normalize` (`v2.compiler.normalize` `normalize_sugar_key_optional`: desugar through the sugar registry to `Validation` + the construction obligation) → `infer` (discharge the obligation at construction sites and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time)."), h2(text: "4. The decidability boundary (the one rule that keeps this §4-legal)"), p(text: "Two tiers, and the split is the whole discipline:"), ul(items: [ @@ -46,13 +45,13 @@ fn cardinality_refinement_body() -> List { li(text: "**Phase-3 — P5 reflection; lift cardinality checks fully static** where the count is known at type level."), ]), h2(text: "6. What one feature unblocks (the ROI)"), - p(text: "Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; `Measure` inhabitance (the deferred `Refined`); typed `|>` coercion (the Measure-inhabitance gap blocked it last week); `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings."), + p(text: "Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; typed `|>` coercion; `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings."), h2(text: "7. Risks / hard parts"), ul(items: [ li(text: "**Decidability discipline** (§4) — the failure mode is P3/P4 quietly admitting a non-cardinality predicate; gate it to the closed vocabulary."), li(text: "**Fold-propagation soundness** — the cardinality a fold computes must be *provably* the real one (a fail-closed witness: a fold that miscounts goes RED)."), - li(text: "**The parser is handwritten** (`bit.dag` header) — `where` lexing/parsing touches the seed parser (load-bearing; sequence behind the §0 lock-down, not during it)."), - li(text: "**P2 is broad** — construction-enforcement touches every construction site of a refined type."), + li(text: "**The parser/normalizer path is load-bearing** — `where` must enter through the modeled grammar and sugar registry, sequenced behind the §0 lock-down."), + li(text: "**P2 completeness is unverified** — audit the existing `sole_constructor` wall across generic carriers, every construction form, and compiler-module exemptions before declaring the attainable ceiling or extending enforcement."), ]), ] } diff --git a/dag/gunbc/plans/compile_clean_forcecheck.dag b/dag/gunbc/plans/compile_clean_forcecheck.dag index 20ff207c152..fe96dfb47d2 100644 --- a/dag/gunbc/plans/compile_clean_forcecheck.dag +++ b/dag/gunbc/plans/compile_clean_forcecheck.dag @@ -2,17 +2,17 @@ module gunbc.plans.compile_clean_forcecheck import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } import std.markdown { MarkdownBlock, TableBlock, AlignNone, AlignRight } -import gunbc.plans.md_helpers { h2, p, li, ul, ol, quote, cell, row } +import gunbc.plans.md_helpers { h2, p, li, ul, ol, cell, row } fn compile_clean_forcecheck_body() -> List { [ - p(text: "**Status:** diagnosis (done, execution-proven) + **(A) partition design** + **blast-radius measured (10 names / 102 sites)**. Scope confirmed by parent `quick-ant-298`: **DESIGN-FIRST + MEASURE-FIRST, land nothing enforcing** — the tree-scoping/registry-partition *flip* is operator-gated (escalates via parent + bright-stag). **DESIGN §5 (fail-closed) is authority.** Work-item `adhoc-6169238c-5e2`. Linked from `ROADMAP.md §0` (line 31, \"inference fail-open — return-type after #5293\") and §1 (floor-coverage). Sibling of [fail-closed-lockdown.md](fail-closed-lockdown.md) §3 (where the pipeline fails open). Adjacent: 2(i) (bright-stag `adhoc-8e5771e1-14a`) grounds `utf8_decode_bytes` as a real std fn — **(A) is what makes such grounding required by construction** so the leak can't recur."), - p(text: "**Verified against the live tree 2026-06-21** — `gunbc` built from `src/v1/stage0`, probes + the empty-registry blast-radius compile run. Line numbers are receipts."), + p(text: "**Status:** historical diagnosis (execution-proven) + live **(A) partition design**. The 10-name / 102-site blast radius is a 2026-06-21 capture, not a live census. **DESIGN §5 (fail-closed) is authority.** Sibling of [fail-closed-lockdown.md](fail-closed-lockdown.md) §3."), + p(text: "**Re-verified against the live tree 2026-07-31.** `v1.compiler.infer_method` `builtin_function_registry` remains a flat global name→type map; `std.encoding` `utf8_decode_bytes` is now grounded and its old registry row is gone. Symbols, not line positions, are receipts."), h2(text: "0. Verdict — the brief's mechanism is wrong; the leak is a global seed allowlist"), - p(text: "The compile-clean gate (`dag/tools/dag_compile_clean_gate.dag` → `gunbc compile --target rust` over `dag/` with `src/v2` as the import pool) is **fail-open**: `gunbc compile` on `main` returns 0 diagnostics / EXIT 0 even though `dag/extdeps/cloud/gcp/secret_manager.dag:71` calls `utf8_decode_bytes`, which is **defined nowhere in `dag/` or `src/v2`**."), - p(text: "The brief framed this as \"unreached fn bodies escape typecheck.\" **That is false** — bodies are always visited. The precise mechanism (execution-proven, §1 below) is two independent fail-open holes:"), + p(text: "At the 2026-06-21 capture, the compile-clean gate (`dag/tools/dag_compile_clean_gate.dag` → `gunbc compile --target rust` over `dag/` with `src/v2` as the import pool) was **fail-open**: `gunbc compile` on `main` returned 0 diagnostics / EXIT 0 even though `extdeps.cloud.gcp.secret_manager` `utf8_secret_from_access_payload` called `utf8_decode_bytes`, which was then **defined nowhere in `dag/` or `src/v2`**. The current tree now defines `std.encoding` `utf8_decode_bytes`; this paragraph is a historical execution receipt, not a claim that the literal leak remains live."), + p(text: "The brief framed this as \"unreached fn bodies escape typecheck.\" **That was false** — bodies were always visited. At the captured run, the execution-proven mechanism (§1 below) was two independent fail-open holes:"), ol(items: [ - li(text: "**Registry leak** — `utf8_decode_bytes` resolves because it is a hardcoded entry in the global `builtin_function_registry()`, an **explicitly-marked BRIDGE scaffold**. The registry is *not scoped to the tree being compiled*, so v1-seed runtime intrinsics leak into the dag-substrate compile."), + li(text: "**Registry leak at capture** — `utf8_decode_bytes` resolved because it was a hardcoded entry in the global `builtin_function_registry()`, then an **explicitly-marked BRIDGE scaffold**. The registry was *not scoped to the tree being compiled*, so v1-seed runtime intrinsics leaked into the dag-substrate compile."), li(text: "**Return-type fail-open** — a function whose body's inferred type ≠ its declared return type is not flagged (`#5293` closed only the record-field hole, not return types). Independent of the gate; a member of ROADMAP §0's \"inference fail-open (return-type after #5293)\"."), ]), h2(text: "1. Execution-proven mechanism (receipts)"), @@ -27,31 +27,26 @@ fn compile_clean_forcecheck_body() -> List { row(cells: [cell(text: "plain return-type mismatch"), cell(text: "`fn f()->Int\{ \"a string\" \}`"), cell(text: "**0 diagnostics**"), cell(text: "declared return type unenforced")]), ], }, - p(text: "**The real on-main witness** — `dag/extdeps/cloud/gcp/secret_manager.dag:70-72`:"), + p(text: "**The real on-main witness** — `extdeps.cloud.gcp.secret_manager` `utf8_secret_from_access_payload`:"), CodeBlock { code: "fn utf8_secret_from_access_payload(payload: Bytes) -> Secret \{\n utf8_decode_bytes(payload: payload) as Secret\n\}\n" }, - p(text: "`utf8_decode_bytes` resolves via the registry; the `as Secret` cast satisfies the return type. So the **literal witness is hole #1 alone** (return-type enforcement would not catch it because of the cast)."), + p(text: "In the captured run, `utf8_decode_bytes` resolved via the registry; the `as Secret` cast satisfied the return type. So the **literal witness was hole #1 alone** (return-type enforcement would not have caught it because of the cast)."), h2(text: "2. The seam — `builtin_function_registry`"), - p(text: "`src/v1/04_method.dag:55-155` (Rust seed `v1_compiler_infer_method.rs:100-365`). 76 names → return-type `Node`s, e.g. `utf8_decode_bytes → string_type` (04_method.dag:93). Its own header is the indictment:"), - quote(blocks: [ - p(text: "`// BRIDGE: This map_insert chain is a duplicate authority over facts that should come from .dag`"), - p(text: "`// function declarations (extern fn signatures). Deletion point: when builtins are actual .dag`"), - p(text: "`// definitions that the compiler loads and resolves, this registry is deleted.`"), - ]), - p(text: "So this is a known §3 fork (duplicate authority) with a **named dissolution trigger**. Two properties make it the fail-open:"), + p(text: "At capture, `v1.compiler.infer_method` `builtin_function_registry` held 76 names → return-type `Node`s, including a `utf8_decode_bytes → string_type` row. That row is absent now, but the live registry remains a flat global map. `std.encoding` `utf8_decode_bytes_host_realization_marker` and `std.bytes` `bytes_seam_host_realization_marker` exist, but both carry a stale `DeclarationRef` to `std.bytes` `builtin_function_registry`, where no such declaration exists. They are unresolved scaffold debt, not verified bindings to the live v1 registry."), + p(text: "The flat live registry remains a known §3 fork (duplicate authority); the two broken marker references are a second §3 gap that must repair or dissolve with it. Two registry properties make the resolution seam fail-open:"), ul(items: [ - li(text: "**Global, not tree-scoped.** The same registry is consulted whether the entry root is `src/v1` (the seed, which legitimately needs `utf8_decode_bytes`/`scan_while`/… as its runtime kernel — used in `05_emit_rust.dag`, `runtime_rust.dag`) or `dag/` (the substrate, which must not depend on seed intrinsics). A name in the registry resolves in *any* tree."), + li(text: "**Global, not tree-scoped.** The same registry is consulted whether the entry root is `src/v1` (the seed, which legitimately needs seed-only intrinsics such as `scan_while`) or `dag/` (the substrate, which must not depend on seed intrinsics). A name in the registry resolves in *any* tree."), li(text: "**Resolution without definition or arg-check.** A registry hit yields a fabricated return type with no parameter typing and no requirement that a definition exist in the compiled closure — DESIGN §5's \"fabricated plausible output\" anti-pattern, at the call-head resolution seam."), ]), - p(text: "(`resolve_builtin_call_type`'s `Absent => unit_type`, 04_method.dag:166, is *not* a live leak for call syntax — unregistered names are caught upstream as \"function not found in scope\". It is a latent fail-open kept for non-call uses; out of scope here, noted for the audit.)"), + p(text: "(`v1.compiler.infer_method` `resolve_builtin_call_type`'s `Absent => unit_type` is *not* a live leak for call syntax — unregistered names are caught upstream as \"function not found in scope\". It is a latent fail-open kept for non-call uses; out of scope here, noted for the audit.)"), h2(text: "3. Construction-correct direction (DESIGN §5/§3)"), - p(text: "The gate's claim is \"the dag substrate is well-typed **and self-contained**.\" Made *unwritable* (§5 construction, not a post-hoc lens): **the set of resolvable builtins must be derived from the tree being compiled, not a global seed allowlist.** This is exactly the registry's own stated deletion point — builtins become real `.dag` definitions resolved through normal import/definition resolution, the global registry is deleted, and a substrate that neither defines nor imports `utf8_decode_bytes` fails closed on it (\"function not found in scope\", identical to probe 2). At that point the leak is dead by construction, not by a roster."), - p(text: "Full dissolution (76 builtins → `.dag` defs) is a large migration, out of this node's scope. The bounded options below are stepping stones; (A) is the one that closes the literal witness *by construction*."), + p(text: "The gate's claim is \"the dag substrate is well-typed **and self-contained**.\" Made *unwritable* (§5 construction, not a post-hoc lens): **the set of resolvable builtins must be derived from the tree being compiled, not a global seed allowlist.** This is exactly the registry's own stated deletion point — builtins become real `.dag` definitions resolved through normal import/definition resolution, the global registry is deleted, and a substrate that neither defines nor imports a live seed-only name such as `scan_while` fails closed on it (\"function not found in scope\", identical to probe 2). At that point the leak is dead by construction, not by a roster."), + p(text: "Full dissolution of the flat registry into `.dag` definitions is a large migration, out of this node's scope. The bounded options below are stepping stones; (A) closes the leak class *by construction*."), h2(text: "4. Scope decision (parent-confirmed) — (A), as design + measure only"), p(text: "Parent `quick-ant-298` confirmed: this node ships **(A)'s design + the blast-radius measurement**, and **lands nothing enforcing**. (B) and (C) are split out:"), ul(items: [ - li(text: "**(A) Tree-scoped builtin availability / registry partition** — the direction. Split the registry into *substrate-available* builtins (real `.dag`/std defs, or the sanctioned primitive surface) and *seed-only kernel* intrinsics; admit the seed-only set only when the entry root is the v1 seed itself. A dag-substrate compile then fails closed on a seed-only name. This **advances the registry's own marked dissolve-on** (04_method.dag:55-62) — it is not new debt. The enforcing flip is **load-bearing** (inference scope) + **changes what compiles** → operator-gated; escalates via parent + bright-stag. This doc + §6's measured number is the input to that sign-off."), - li(text: "**(B) Return-type enforcement** — SEPARATE (ROADMAP §0 line 31; #5293 closed only record-field). Does not close the literal witness (the `as Secret` cast satisfies the return type). Its own PR later. Flagged adjacent, not bundled."), - li(text: "**(C) Grounding `utf8_decode_bytes` as a real std fn** — **2(i)'s job** (bright-stag `adhoc-8e5771e1-14a`). Nuance relayed: `utf8_decode_bytes` is a *registry entry* (→ `string_type`), not purely undefined — so 2(i) must define the std fn **and** delete its registry bridge row, else the registry shadows the new def. (A) is what makes that grounding *required* by construction."), + li(text: "**(A) Tree-scoped builtin availability / registry partition** — the live direction. Split the registry into *substrate-available* builtins (real `.dag`/std defs, or the sanctioned primitive surface) and *seed-only kernel* intrinsics; admit the seed-only set only when the entry root is the v1 seed itself. A dag-substrate compile then fails closed on a seed-only name. The enforcing flip is **load-bearing** (inference scope) + **changes what compiles** → operator-gated; it must also repair or dissolve the stale marker `DeclarationRef`s rather than treating them as authority."), + li(text: "**(B) Return-type enforcement** — separate. It did not close the historical literal witness because the `as Secret` cast satisfied the return type; do not bundle it with registry partitioning."), + li(text: "**(C) Grounding `utf8_decode_bytes` as a real std fn — complete.** `std.encoding` now declares `utf8_decode_bytes`, and the historical registry row is gone. Its host realization still carries `utf8_decode_bytes_host_realization_marker`, which dissolves with the registry fork."), ]), h2(text: "5. (A) partition design"), p(text: "**Two facts must be separated** at the call-head builtin-resolution seam:"), @@ -61,7 +56,7 @@ fn compile_clean_forcecheck_body() -> List { ]), p(text: "**Construction shape (the registry's dissolve-on, staged):** each builtin row carries an **availability tag** — `SubstrateAvailable` vs `SeedOnly` — instead of a flat name→type map. The call-head resolver admits a `SeedOnly` row **only when the compile's entry root is the v1 seed**; for a substrate entry root (dag/ + v2 pool) a `SeedOnly` hit is treated as *not a builtin* → falls through to the existing fail-closed \"function not found in scope\" (probe 2). `SubstrateAvailable` rows are the sanctioned primitive surface and, per the dissolve-on, migrate to real `std` `.dag` defs over time; once a name has a real def it leaves the registry entirely and resolves through normal func-env lookup."), ul(items: [ - li(text: "*Entry-root signal*: the existing entry-vs-pool distinction (`main.rs:343-347` \"entry modules = all .dag in the FIRST source root; additional roots are dependency pools\") already separates the compiled tree from its pools. The infer scope must carry one bit — \"entry root is the v1 seed\" — derived from whether `src/v1` is the primary `--source-root`. (Threading this into `InferScope` is the load-bearing part; out of scope for this node — captured here for the enforce PR.)"), + li(text: "*Entry-root signal*: the existing entry-vs-pool distinction (`v1.compiler.emit_rust` `emit_compile_match_arm`: \"entry modules = all .dag in the FIRST source root; additional roots are dependency pools\") already separates the compiled tree from its pools. The infer scope must carry one bit — \"entry root is the v1 seed\" — derived from whether `src/v1` is the primary `--source-root`. (Threading this into `InferScope` is the load-bearing part; out of scope for this node — captured here for the enforce PR.)"), li(text: "*Why a tag, not a second map*: a second allowlist map would be a new parallel authority (§3). One row per builtin with an availability field keeps single authority and reads as construction, not a lens."), li(text: "*Non-enforcing intermediate (this node)*: the empty-registry measurement in §6 already enumerates the exact leak set without any code change shipping. The enforce PR turns each `SeedOnly` substrate hit into the fail-closed path behind operator sign-off."), ]), @@ -79,14 +74,14 @@ fn compile_clean_forcecheck_body() -> List { row(cells: [cell(text: "`set_contains`"), cell(text: "3"), cell(text: "dag/std"), cell(text: "set primitive")]), row(cells: [cell(text: "`set_insert`"), cell(text: "2"), cell(text: "dag/std"), cell(text: "set primitive")]), row(cells: [cell(text: "`count`"), cell(text: "2"), cell(text: "dag/gunbc/tools"), cell(text: "general primitive")]), - row(cells: [cell(text: "`utf8_decode_bytes`"), cell(text: "1"), cell(text: "**dag/extdeps/cloud/gcp**"), cell(text: "**the brief's witness — true domain leak (2(i) grounds it)**")]), + row(cells: [cell(text: "`utf8_decode_bytes`"), cell(text: "1"), cell(text: "**dag/extdeps/cloud/gcp**"), cell(text: "**historical brief witness — domain leak later grounded under completed (C)**")]), row(cells: [cell(text: "`hash_combine`"), cell(text: "1"), cell(text: "dag/std"), cell(text: "hashing primitive")]), row(cells: [cell(text: "`atom_identity_hash`"), cell(text: "1"), cell(text: "dag/std"), cell(text: "hashing primitive")]), ], }, - p(text: "**Reading of the number:** the (A) rollout is **small and tractable**, not a corpus-wide flag day. 8 of the 10 (96 sites) are the accepted general-purpose primitive surface (`string_contains`, `to_string`, `concat`, `count`, `set_contains`, `set_insert`, `hash_combine`, `atom_identity_hash`) — these become `SubstrateAvailable` and are the std-grounding backlog. `filesystem_read` (5) is the already-known lens reflection fork. Exactly **one** name — `utf8_decode_bytes` — is a genuine domain leak, and it is already owned by 2(i). So (A) tags 8–9 substrate primitives + the lens-reflection intrinsic, and the only domain code that fails closed under (A) today is the single gcp site, which 2(i) is already grounding. The blast radius gates the rollout: tag the 8 primitives `SubstrateAvailable` first (no breakage), then flip seed-only enforcement once `utf8_decode_bytes` is grounded."), + p(text: "**Reading of the captured number:** on 2026-06-21, 8 of the 10 names (96 sites) were general-purpose primitive calls (`string_contains`, `to_string`, `concat`, `count`, `set_contains`, `set_insert`, `hash_combine`, `atom_identity_hash`), `filesystem_read` (5) was the known lens-reflection fork, and `utf8_decode_bytes` (1) was the sole domain leak. Completed (C) has since grounded `std.encoding` `utf8_decode_bytes` and removed its registry row, so this capture does **not** identify a live domain-code failure or establish today's rollout size. Before enforcing (A), re-run the real compile measurement against the current registry, classify each remaining live row as `SubstrateAvailable` or `SeedOnly`, then prove the partition with the `scan_while` red in §7."), h2(text: "7. Discriminating witness (must go RED when the behavior is wrong)"), - p(text: "The enforce PR's receipt is the same shape as §6's method: a planted substrate module that free-calls a `SeedOnly` builtin (`utf8_decode_bytes`) must make `gunbc compile` over the dag pools **fail**; the identical module compiled with the `src/v1` seed as primary root must **pass**. Green-by-execution against the real `gunbc`, not a typecheck/grep. (DESIGN §5: spec-without-execution is not done.)"), + p(text: "The enforce PR's receipt is the same shape as §6's method: a planted substrate module that free-calls a live seed-only builtin such as `scan_while` must make `gunbc compile` over the dag pools **fail**; the identical call compiled under the `src/v1` seed must **pass**. Green-by-execution against the real `gunbc`, not a typecheck/grep. (DESIGN §5: spec-without-execution is not done.)"), ] } @@ -95,6 +90,6 @@ data compile_clean_forcecheck_plan: Plan = Plan { title: "Plan — compile-clean gate force-check (ROADMAP §1 floor-coverage / §0 inference fail-open)", body: compile_clean_forcecheck_body(), dissolution: HasTrigger { - text: "Delete this doc when (A) lands as construction: the builtin registry carries a `SubstrateAvailable`/`SeedOnly` availability tag, a dag-substrate compile fails closed on a seed-only name (the §7 discriminating witness green-by-execution — a planted `utf8_decode_bytes` call fails over the dag pools and passes under the v1-seed root), and `utf8_decode_bytes` is grounded as a real std def with its registry bridge row deleted — at which point the leak is dead by construction (DESIGN §5), the registry's own marked dissolve-on (04_method.dag:55-62) has advanced, and this design+measurement doc is superseded by the wall it specified." + text: "Delete this doc when (A) lands as construction: the builtin registry carries a `SubstrateAvailable`/`SeedOnly` availability tag, a dag-substrate compile fails closed on a live seed-only name such as `scan_while` while the v1 seed admits it, and the stale `DeclarationRef`s in `utf8_decode_bytes_host_realization_marker` / `bytes_seam_host_realization_marker` are repaired onto a live authority or dissolve — at which point the leak is dead by construction (DESIGN §5)." } } diff --git a/dag/gunbc/plans/format_model_reconciliation.dag b/dag/gunbc/plans/format_model_reconciliation.dag index 3c60855253e..59eb4d32a16 100644 --- a/dag/gunbc/plans/format_model_reconciliation.dag +++ b/dag/gunbc/plans/format_model_reconciliation.dag @@ -6,60 +6,60 @@ import gunbc.plans.md_helpers { h2, h3, p, li, ul, ol, cell, row } fn format_model_reconciliation_body() -> List { [ - BlockquoteBlock { blocks: [p(text: "Record-spelling reconciliation: one concept — how a format spells records — was forked across three models, and no text format routes serialization through any of them today. DESIGN refs: §2 (one concept every scale — decompress the leaf, map to existing carriers, reduce duplicates), §3 (single authority — field-by-field decomposition onto ConfigFormat, CommentSyntax, LayoutProtocol; delete uninhabited scaffolds), §5 (construction over validation — the swap test is execution-grounded), §6 (complementary to [regime-2 shared emission fold](regime2-shared-emission-fold.md), not a parallel ledger).")] }, - p(text: "**Status:** planning tracker · **`.dag` carrier is authority** (§6). Linked from `ROADMAP.md` §6 cross-media band. Carrier facts verified against the live tree 2026-06-30. **Code keystone:** still-wolf-292 / PR #6045 (C1) — this doc captures only; no serializer code here."), - h2(text: "1. The fork — three models, zero routed serializers"), + BlockquoteBlock { blocks: [p(text: "Record-spelling reconciliation: one concept — how a format spells records — was historically forked across three models. The live tree has dissolved the two legacy models into `ConfigFormat`, `CommentSyntax`, `LayoutProtocol`, and `SerializationKnobs`; this tracker now owns only the remaining emitter migrations. DESIGN refs: §2 (one concept every scale), §3 (single authority), §5 (execution-grounded swap test), §6 (complementary to [regime-2 shared emission fold](regime2-shared-emission-fold.md), not a parallel ledger).")] }, + p(text: "**Status:** implementation tail · **`.dag` carrier is authority** (§6). Carrier facts re-verified against the live tree 2026-07-31."), + h2(text: "1. The historical fork and its live resolution"), p(text: "Layout (line/indent/newline) is [regime-2 shared emission fold](regime2-shared-emission-fold.md). **This doc owns record spelling** — how key/value, assign, quoting, and nesting render into text or JSON:"), TableBlock { header: row(cells: [cell(text: "model"), cell(text: "where"), cell(text: "role"), cell(text: "verdict")]), alignments: [AlignNone, AlignNone, AlignNone, AlignNone], rows: [ - row(cells: [cell(text: "`ConfigFormat`"), cell(text: "`dag/std/languages.dag`"), cell(text: "format **identity** (id, name, extensions, comment)"), cell(text: "**keep**")]), - row(cells: [cell(text: "`FormatModel`"), cell(text: "`dag/std/languages.dag:36`"), cell(text: "indent, max_line_width, import_grouping, trailing_newline"), cell(text: "**uninhabited dead scaffold** — delete")]), - row(cells: [cell(text: "`OutputFormat`"), cell(text: "`dag/std/render.dag:160`"), cell(text: "name, indent_unit, kv_separator, list_prefix, comment_prefix, section_separator, trailing_newline"), cell(text: "**only live knob record** — sole consumer `gitignore_output_format`; `comment_prefix` is a §3 nickname of `CommentSyntax.line_prefix`")]), + row(cells: [cell(text: "`ConfigFormat`"), cell(text: "`std.languages` `ConfigFormat`"), cell(text: "format identity plus optional record knobs"), cell(text: "**live authority**")]), + row(cells: [cell(text: "`FormatModel`"), cell(text: "absent from the live tree"), cell(text: "legacy layout scaffold"), cell(text: "**deleted**")]), + row(cells: [cell(text: "`OutputFormat`"), cell(text: "absent from the live tree"), cell(text: "legacy mixed layout/record knobs"), cell(text: "**deleted and decomposed**")]), ], }, - p(text: "No text format today routes record serialization through any of these types — emitters hand-roll `concat` / `match` per site."), + p(text: "`std.languages` `SerializationKnobs` and `std.serialize` `serialize_record_doc` now carry record spelling. `gunbc.runner_deploy_emit` routes manifest and JSON projections through them; remaining boutique emitters are scoped below."), h2(text: "2. The decomposition — map each field to its single authority (§3)"), - p(text: "Decompose `OutputFormat` field-by-field onto existing carriers; the irreducible residue is the record-spelling knobs only:"), + p(text: "The deleted `OutputFormat` was decomposed field-by-field onto existing carriers; the irreducible residue is the record-spelling knobs only:"), ul(items: [ li(text: "`name` → `ConfigFormat` (identity already lives there)"), li(text: "`comment_prefix` → `CommentSyntax.line_prefix` (derive `#` from format comment, never duplicate)"), li(text: "`indent_unit`, `trailing_newline` → `std.layout.LayoutProtocol` (line-layout half; owned by regime-2)"), li(text: "**Residue → `SerializationKnobs`** in `std.languages`: assign separator, entry separator, open/close delimiters, quoting policy — a comment-free record-spelling value"), ]), - p(text: "**Target pipeline:** a total `serialize_record` fold producing `std.layout.Doc` (recursive — JSON/proto nesting fits). Compose with regime-2 `render(doc, protocol)` for the line half."), + p(text: "**Live pipeline:** `std.serialize` `serialize_record_doc` produces `std.layout` `Doc` recursively; compose it with `std.layout` `render` for the line half."), CodeBlock { code: "doc = serialize_record(record, knobs) // record half (this doc)\ntext = render(doc, layout_protocol) // line half (regime-2)\n" }, h3(text: "The swap test (acid test)"), - p(text: "The **same** record projection renders as manifest text **and** JSON by swapping only the `SerializationKnobs` value — one `serialize_record`, two knob instances, byte-identical witnesses. This is the substrate that makes JSON-as-first-class real under §6 cross-media."), + p(text: "`test.claim.config_record_emit_witness` and `test.claim.runner_placement_witness` exercise the same record projection with manifest and JSON knob values. This is the execution-grounded substrate for JSON-as-first-class under §6 cross-media."), h3(text: "Relationship to regime-2 (complementary, not duplicate)"), ul(items: [ li(text: "[regime-2 shared emission fold](regime2-shared-emission-fold.md) — **line-layout half**: one `render(doc, protocol)` fold over `std.layout.Doc` for yaml/gitignore/runner-deploy/ci.yml projections."), li(text: "**This doc — record-spelling half**: `serialize_record` → `Doc`, then regime-2 renders. Cross-reference only; do not merge the plans."), ]), - h2(text: "3. Hazard — do not build on `std.render` kv helpers"), - p(text: "`std.render` `kv_pair` / `kv_block` are **broken** for real emission: in `.dag` runtime literals bare curly-brace interpolation is live, while the escaped-brace form in `render.dag:119-120` emits literal brace characters, not key=value pairs. `digest_render.dag` and friends must route through `serialize_record`, not these helpers."), - h2(text: "4. Ordered scope (C1–C6)"), + h2(text: "3. Boundary — `std.render` kv helpers are presentation utilities"), + p(text: "`std.render` `kv_pair` and `kv_block` correctly render caller-supplied separators, but they do not carry format-owned `SerializationKnobs` or recursive record structure. Keep them for presentation-only key/value lists; record emitters such as manifest and JSON projections route through `std.serialize` `serialize_record_doc`."), + h2(text: "4. Ordered scope (completed foundation, then remaining tail)"), ol(items: [ - li(text: "**C1 (keystone — still-wolf-292 / PR #6045):** `SerializationKnobs` residue in `std.languages` + recursive `serialize_record` → `Doc` + delete `FormatModel`; migrate runner manifest (`dag/gunbc/runner_deploy_emit.dag` — `manifest_host_text` / `session_host_text` / `operating_row_text`) byte-identically; JSON knobs instance + swap-test witness."), - li(text: "**C2 (folded into C1):** runner manifest + JSON as the first proving instance — not a separate roadmap row."), - li(text: "**C3:** gitignore de-fork — migrate live `OutputFormat` consumer (`dag/gunbc/gitignore_emit.dag` + `extdeps/git/gitignore.dag`) onto `SerializationKnobs` + `ConfigFormat`, derive `#` via `CommentSyntax`, then **delete `OutputFormat`** and orphan `extdeps/git/gitignore_render.dag` (declares knobs then ignores them)."), - li(text: "**C4:** dnsmasq emit — add dnsmasq `ConfigFormat` + knobs; keep cited positional micro-syntax honest (do not force pure key=value)."), - li(text: "**C5 (low):** digest/accelerator kv blocks (`dag/gunbc/digest_render.dag` and friends) — route through `serialize_record`; supersedes broken `std.render` kv helpers."), - li(text: "**C6 (cosmetic):** CSS declaration blocks — `dag/gunbc/roadmap_style.dag` `css_rule(selector, props)` has `props` as raw `String` (`css_rule_props_scaffold`); flat `property:value` records (assign `: `, separator `; `) are `serialize_record` candidates; selector nesting stays structural. Plus yaml/markdown/html identity-link cosmetics."), + li(text: "**C1 complete:** `std.languages` `SerializationKnobs` + recursive `std.serialize` `serialize_record_doc` → `Doc`; `FormatModel` deleted; `gunbc.runner_deploy_emit` manifest fields migrated byte-identically."), + li(text: "**C2 complete (folded into C1):** runner manifest + JSON are the first proving instance, witnessed by `test.claim.config_record_emit_witness` and `test.claim.runner_placement_witness`."), + li(text: "**C3 complete:** `OutputFormat` and the orphan gitignore renderer are absent. `gunbc.gitignore_emit` derives comments from `std.languages` `gitignore_format` and renders a `Doc` with its `gitignore_protocol`; because gitignore is a line-list rather than a record, it does not acquire fake `SerializationKnobs`."), + li(text: "**C4 complete at the honest boundary:** `extdeps.formats.dnsmasq` projects directives to `Doc` with `dnsmasq_protocol`; its positional micro-syntax remains explicit rather than being forced into a key/value record."), + li(text: "**C5 (low):** classify digest/accelerator key/value blocks (`gunbc.digest_render` and `gunbc.accelerator_demo_render`) by semantic grain: presentation-only lists stay on the correct `std.render` helpers; true record projections route through `std.serialize` `serialize_record_doc` with byte-identical witnesses."), + li(text: "**C6 complete:** `gunbc.roadmap_style` now uses typed `CssDecl` rows on shared `BuildRule` machinery; the old `css_rule_props_scaffold` remains only as historical text in its dissolution note."), ]), - h2(text: "5. Audit receipts (live tree 2026-06-30)"), + h2(text: "5. Audit receipts (live tree 2026-07-31)"), ul(items: [ - li(text: "`FormatModel` at `languages.dag:36` — type only, zero `data` rows, not in `LanguageSpec`."), - li(text: "`OutputFormat` at `render.dag:160` — consumed by `extdeps/git/gitignore.dag` `gitignore_output_format` only."), - li(text: "`extdeps/git/gitignore_render.dag` — orphan knob declarations, ignored at emit."), - li(text: "`languages_consumer_census` baselines: 71 total decls, 64 language rows, 7 format rows (`src/v2/lens/languages_consumer_census.dag:9-11`)."), + li(text: "No `FormatModel`, `OutputFormat`, `gitignore_output_format`, or `gitignore_render` declaration remains in the live tree."), + li(text: "`std.languages` `ConfigFormat.record` carries optional `SerializationKnobs`; `json_record_knobs` is a live instance."), + li(text: "`std.serialize` `serialize_record_doc` is the recursive record-spelling fold; `gunbc.runner_deploy_emit` is its live manifest/JSON consumer."), + li(text: "`v2.lens.languages_consumer_census` baselines: `languages_consumer_census_data_decl_baseline`, `languages_consumer_census_per_language_row_baseline`, `languages_consumer_census_format_row_baseline`."), ]), h2(text: "6. Open / boundaries"), ul(items: [ - li(text: "C1 code lands in still-wolf-292 / PR #6045 — this capture PR is docs + roadmap authority only."), + li(text: "The remaining work is emitter migration, not another model declaration."), li(text: "Regime-1 grammar-inverse language emit stays out of scope (v2 `TargetModel` rows)."), - li(text: "`import_grouping` on deleted `FormatModel` — language-emit-only if it survives at all; do not carry into `SerializationKnobs`."), + li(text: "Language-emission `import_grouping` stays outside `SerializationKnobs`."), ]), ] } @@ -69,6 +69,6 @@ data format_model_reconciliation_plan: Plan = Plan { title: "Format-model reconciliation — record spelling onto single authority", body: format_model_reconciliation_body(), dissolution: HasTrigger { - text: "Delete this doc when all three knob models are collapsed into one: FormatModel deleted, OutputFormat dissolved into ConfigFormat + CommentSyntax + LayoutProtocol + SerializationKnobs, and every record-emitting format routes through serialize_record — byte-identical-witnessed on runner manifest, gitignore, and the manifest-text vs JSON swap test." + text: "Delete this doc when the C5 digest/accelerator tail is classified by semantic grain and every true record projection routes through `std.serialize` `serialize_record_doc` with byte-identical witnesses; presentation-only lists explicitly remain on `std.render`. The legacy FormatModel/OutputFormat collapse, runner manifest/JSON swap, gitignore line-layout de-fork, dnsmasq boundary, and CSS typed-row migration are already complete." } } diff --git a/dag/gunbc/plans/language_target_self_host_frontier.dag b/dag/gunbc/plans/language_target_self_host_frontier.dag index 3fe31ba5d7f..f3cae72a5f9 100644 --- a/dag/gunbc/plans/language_target_self_host_frontier.dag +++ b/dag/gunbc/plans/language_target_self_host_frontier.dag @@ -27,17 +27,16 @@ fn language_target_self_host_frontier_body() -> List { rows: [ row(cells: [cell(text: "**F0**"), cell(text: "`emit` / `emit_module` pipeline (walks TargetModel edges backward; new target = rows, no pipeline edit)"), cell(text: "✓ done")]), row(cells: [cell(text: "**F1**"), cell(text: "`TargetModel` 4-edge + grammar-inverse translation rows"), cell(text: "✓ done")]), - row(cells: [cell(text: "**F2**"), cell(text: "VEP (`TargetValueExpressionProjection`) — the general body producer"), cell(text: "**partial** (rust: `^rust_token_unwired_\{else,loop,match,fat_arrow\}`, `rust.dag:1148-1176`) · partial (TS: match/loop/bind-in unwired) · **absent** (python, ecmascript)")]), + row(cells: [cell(text: "**F2**"), cell(text: "VEP (`TargetValueExpressionProjection`) — the general body producer"), cell(text: "**partial** (rust: `^rust_token_unwired_\{else,loop,match,fat_arrow\}`, `v2.extdeps.languages.rust` `rust_value_expression_projection`) · partial (TS: match/loop/bind-in unwired) · **absent** (python, ecmascript)")]), row(cells: [cell(text: "**F3**"), cell(text: "`BlockEvaluationMode` statement spine (`ValueProducing` vs `StatementSequenced`)"), cell(text: "✓ type exists; TS's `StatementSequenced` arm produces the correct fail-closed refusals")]), - row(cells: [cell(text: "**F4**"), cell(text: "`ProcessProgram` transport + `run_emit_host`; executable identity **bound per extdeps transport row** (`HostTransportDescriptor` / `ProcessProgram`, `host_transport.dag`), compiler dispatch **generic**"), cell(text: "✓ machinery; **DEFECT: dispatch is a central switch** — `host_tool_program_name` (`emit_host.dag:164-172`) is `if cargo … else if cc … else reject`, so every new tool edits one function (contradicts F0). Fix = row-bound exe identity + generic dispatch, **not** another switch branch")]), - row(cells: [cell(text: "**F5**"), cell(text: "self-host frontier runner (`run_test_claim_module_emit_vs_eval`: emit → build → run → compare-to-eval)"), cell(text: "✓ machinery **for Rust only**, run **OFFLINE** (excluded from discovery). Rust is **not** self-hosted: `compiler_frontier_self_emitted_baseline = 0` of `compiler_frontier_module_count_expected = 27` (`src/v2/compiler/self_host/frontier.dag`)")]), + row(cells: [cell(text: "**F4**"), cell(text: "`ProcessProgram` transport + `run_emit_host`; executable identity **bound per extdeps transport row** (`v2.std.host_transport` `HostTransportDescriptor` / `ProcessProgram`), compiler dispatch **generic** (`v2.compiler.emit_host` `process_program_name`)"), cell(text: "✓ done — `HostToolProgram.executable` is carried by the row and generic dispatch returns that value; target-specific work is only to configure a runtime row where one is absent")]), + row(cells: [cell(text: "**F5**"), cell(text: "self-host frontier runner (`v2.compiler.emit_host` `run_test_claim_module_emit_vs_eval`: emit → build → run → compare-to-eval)"), cell(text: "✓ machinery **for Rust only**, run **OFFLINE** (excluded from discovery). Rust is **not** self-hosted: `v2.compiler.self_host.frontier` `compiler_frontier_emitter_produced_count` is pinned to `v2.compiler.self_host.emitter_producer_provenance` `emitter_produced_baseline = 0`; `v2.compiler.self_host.frontier` `compiler_frontier_roster_count` derives the roster size.")]), row(cells: [cell(text: "**F6**"), cell(text: "`solve` — **structural** = existing `solve_constraints` / `ConstraintGraph` authority (extend, no fork); **numerical** = *absent* typed gap (finite measure + `TerminationProof`, typed residual-acceptance contract, extdeps solver handler)"), cell(text: "**off critical path** — not needed for emit-to-simulator; see solve doc")]), - row(cells: [cell(text: "**F7**"), cell(text: "declaration emission generic over target (`emit_semantic_decl.dag`)"), cell(text: "**FORKED — `emit_semantic_decl.dag` is rust-hardwired**; de-fork to row-driven per-target decl spellings is a front-loaded barrier, sibling to the F4 de-fork")]), + row(cells: [cell(text: "**F7**"), cell(text: "declaration emission generic over target (`v2.compiler.emit_semantic_decl` `emit_semantic_type_decl`)"), cell(text: "✓ done — the declaration emitter accepts a `TargetModel` and reads its emission bundle through `v2.std.compilers.semantic_decl_emission` `semantic_decl_emission_from_target`")]), ], }, - h3(text: "The two highest-leverage shared dependencies (do these once, everyone inherits)"), + h3(text: "The highest-leverage shared dependencies (do these once, everyone inherits)"), ol(items: [ - li(text: "**F4 exe-identity de-fork** — today executable identity is chosen by a central `host_tool_program_name` switch (`emit_host.dag:164-172`: `if cargo … else if cc … else reject`), which gates **bar-c for every language** and forces a branch edit per tool (contradicts F0's \"new target = rows, no pipeline edit\"). Bind exe identity in each extdeps transport row (`HostTransportDescriptor` / `ProcessProgram`, `host_transport.dag`) and make compiler dispatch **generic**; then each target's *already-declared* runtime row runs through the typed self-host path with no pipeline edit. Highest-leverage de-fork on the board. **F7 (decl-emission de-fork of the rust-hardwired `emit_semantic_decl.dag`) is its sibling barrier.**"), li(text: "**F2 VEP completion** — wire the unwired forms **once** (rust's `^rust_token_unwired_\{else,loop,match,fat_arrow\}`; TS's match / loop / bind-in) in the `StatementSequenced` arm; the family inherits body breadth. Python additionally needs its *first* VEP edge."), ]), hr(), @@ -46,27 +45,27 @@ fn language_target_self_host_frontier_body() -> List { header: row(cells: [cell(text: "target"), cell(text: "family"), cell(text: "current bar (verified)"), cell(text: "honest end-state"), cell(text: "key deps"), cell(text: "stress axis")]), alignments: [AlignNone, AlignNone, AlignNone, AlignNone, AlignNone, AlignNone], rows: [ - row(cells: [cell(text: "**rust**"), cell(text: "compiled"), cell(text: "compiled; bar-c; F2 **partial** (`^rust_token_unwired_\{else,loop,match,fat_arrow\}`, `rust.dag:1148-1176`); F5 emit-vs-eval fixture **OFFLINE**"), cell(text: "**`SeedRetained` — 0/27 self-emitted** (`compiler_frontier_self_emitted_baseline = 0`, `frontier.dag`); reference model, **NOT self-hosted**"), cell(text: "F2 completion; F5 self-host generalization"), cell(text: "(reference model)")]), - row(cells: [cell(text: "**cpp — Phase-0-C**"), cell(text: "compiled"), cell(text: "bar-c via `cc`, proven by an **OFFLINE** witness in `test/claim/execution/` (excluded from discovery)"), cell(text: "bar-c green (offline); self-host N/A at this phase"), cell(text: "F4(`cc`) row-bound, F5-generalize"), cell(text: "(confirms)")]), + row(cells: [cell(text: "**rust**"), cell(text: "compiled"), cell(text: "compiled; bar-c; F2 **partial** (`^rust_token_unwired_\{else,loop,match,fat_arrow\}`, `v2.extdeps.languages.rust` `rust_value_expression_projection`); F5 emit-vs-eval fixture **OFFLINE**"), cell(text: "**`SeedRetained` roster; zero producer-qualified emissions** — `v2.compiler.self_host.frontier` `compiler_frontier_emitter_produced_count` equals `v2.compiler.self_host.emitter_producer_provenance` `emitter_produced_baseline = 0`, and `seed_emitter_behavioral_green_count` equals `seed_emitter_behavioral_green_baseline = 0`; reference model, **NOT self-hosted**"), cell(text: "F2 completion; F5 self-host generalization"), cell(text: "(reference model)")]), + row(cells: [cell(text: "**cpp — Phase-0-C**"), cell(text: "compiled"), cell(text: "bar-c via `cc`, proven by an **OFFLINE** witness in `test/claim/execution/` (excluded from discovery)"), cell(text: "bar-c green (offline); self-host N/A at this phase"), cell(text: "F5-generalize"), cell(text: "(confirms)")]), row(cells: [cell(text: "**cpp — full C target**"), cell(text: "compiled"), cell(text: "**below bar-a** for full C"), cell(text: "blocked — needs **monomorphization** (grep-**zero** in tree), **closure conversion**, a **discriminant-tag row kind**, **multi-file (header/impl) projection**, and **ABI/linkage** — none present"), cell(text: "monomorphization, closure conversion, tag-row kind, multi-file projection, ABI/linkage"), cell(text: "(confirms — hard)")]), - row(cells: [cell(text: "**go**"), cell(text: "compiled"), cell(text: "**skeleton** — needs TargetModel buildout"), cell(text: "**self-host** (first non-rust self-host — the F5 generalization proof), once built"), cell(text: "TargetModel buildout, F4(`go`) row-bound, surface spellings, F5"), cell(text: "**self-host axis**")]), - row(cells: [cell(text: "**java / kotlin / swift**"), cell(text: "compiled"), cell(text: "**skeleton** — need TargetModel buildout"), cell(text: "bar-c → self-host"), cell(text: "TargetModel buildout, F4(tool) row-bound, spellings, inherit F2/F3/F5"), cell(text: "(confirms — parallel)")]), - row(cells: [cell(text: "**typescript**"), cell(text: "interpreted"), cell(text: "F2 **partial** (match/loop/bind-in unwired); **bar-c RED** — runtime row present but `node`/`npx` unregistered"), cell(text: "self-host"), cell(text: "F4(`node`/`npx`) row-bound, F2 completion (match/loop/bind-in), operator catalog"), cell(text: "self-host axis")]), - row(cells: [cell(text: "**python**"), cell(text: "interpreted"), cell(text: "**no VEP edge — add-only**"), cell(text: "bar-c → self-host"), cell(text: "F2 *first* edge, operator catalog, F4(`python3`) row-bound"), cell(text: "self-host axis")]), + row(cells: [cell(text: "**go**"), cell(text: "compiled"), cell(text: "**skeleton** — needs TargetModel buildout"), cell(text: "**self-host** (first non-rust self-host — the F5 generalization proof), once built"), cell(text: "TargetModel buildout, surface spellings, F5"), cell(text: "**self-host axis**")]), + row(cells: [cell(text: "**java / kotlin / swift**"), cell(text: "compiled"), cell(text: "**skeleton** — need TargetModel buildout"), cell(text: "bar-c → self-host"), cell(text: "TargetModel buildout, runtime-row configuration, spellings, inherit F2/F3/F5"), cell(text: "(confirms — parallel)")]), + row(cells: [cell(text: "**typescript**"), cell(text: "interpreted"), cell(text: "F2 **partial** (match/loop/bind-in unwired); runtime row is configured (`v2.extdeps.languages.typescript` `ts_runtime_row`), but this pre-un-shelve map does not establish current bar-c execution"), cell(text: "self-host"), cell(text: "F2 completion (match/loop/bind-in), operator catalog"), cell(text: "self-host axis")]), + row(cells: [cell(text: "**python**"), cell(text: "interpreted"), cell(text: "**no VEP edge — add-only**"), cell(text: "bar-c → self-host"), cell(text: "F2 *first* edge, operator catalog"), cell(text: "self-host axis")]), row(cells: [cell(text: "**ecmascript**"), cell(text: "interpreted"), cell(text: "**orphan (0 consumers)**"), cell(text: "**decide first**: adopt as TS's JS base, or delete"), cell(text: "(adoption decision)"), cell(text: "—")]), row(cells: [cell(text: "**lean**"), cell(text: "expression/ML"), cell(text: "**below bar-a** — type model + anchor test only, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs)"), cell(text: "self-host on an *expression* spine (not statement), once a TargetModel is built"), cell(text: "committed TargetModel, F3 generalization (expression-mode), F2, F5"), cell(text: "self-host axis (spine falsifier)")]), - row(cells: [cell(text: "**verilog**"), cell(text: "HDL"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel**; **11** `body_lexeme:String` fields to decompose"), cell(text: "**bar-c green + frontier row `self-host: N/A (hardware)`**"), cell(text: "committed TargetModel, decompose `body_lexeme` → structured, F4(`verilator`/`iverilog`) row-bound"), cell(text: "**emit-generality (concurrent)**")]), - row(cells: [cell(text: "**spice**"), cell(text: "analog format"), cell(text: "**bar-b only** — the witness compares emitted text to a **golden** (`spice_rc_ngspice_oracle_test.dag:18-25`); it **never runs ngspice**"), cell(text: "bar-c green + frontier row `self-host: N/A (analog)`. **No Modelica carrier in-tree** — dual-emit is future, not present"), cell(text: "F4(`ngspice`) row-bound (bar-b → bar-c); Modelica carrier does not yet exist"), cell(text: "**emit-generality (continuous)**")]), - row(cells: [cell(text: "**llvm_ir**"), cell(text: "IR/backend"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs)"), cell(text: "bar-c green + frontier row `self-host: N/A (no runtime)` — the Rust/cargo-free lowering path, once a TargetModel is built"), cell(text: "committed TargetModel, F4(`llc`/`clang`) row-bound"), cell(text: "**emit-generality (SSA)**")]), - row(cells: [cell(text: "**wasm**"), cell(text: "IR/backend"), cell(text: "has a **TargetModel** (bundle/lex/binding_spellings) BUT **bar-c unreachable** — `runtime_row: target_emit_host_runtime_row_unconfigured` (HostRuntimeRowAbsent, `wasm.dag:624-632`)"), cell(text: "bar-c green + frontier row `self-host: N/A` — **blocked on configuring the runtime row**"), cell(text: "configure runtime row, F4(`wasmtime`) row-bound"), cell(text: "emit-generality (stack machine)")]), - row(cells: [cell(text: "**machine_code / ptx**"), cell(text: "ISA/GPU"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs)"), cell(text: "bar-c green + frontier row `self-host: N/A`, once a TargetModel is built"), cell(text: "committed TargetModel, F4(assembler/`ptxas`) row-bound"), cell(text: "emit-generality (ISA)")]), + row(cells: [cell(text: "**verilog**"), cell(text: "HDL"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel**; **11** `body_lexeme:String` fields to decompose"), cell(text: "**bar-c green + frontier row `self-host: N/A (hardware)`**"), cell(text: "committed TargetModel, decompose `body_lexeme` → structured, configure the `verilator`/`iverilog` runtime row"), cell(text: "**emit-generality (concurrent)**")]), + row(cells: [cell(text: "**spice**"), cell(text: "analog format"), cell(text: "**bar-b only** — the witness compares emitted text to a **golden** (`v2.test.formats.spice_rc_ngspice_oracle` `spice_rc_ngspice_op_holds`); it **never runs ngspice**"), cell(text: "bar-c green + frontier row `self-host: N/A (analog)`. **No Modelica carrier in-tree** — dual-emit is future, not present"), cell(text: "configure the `ngspice` runtime row (bar-b → bar-c); Modelica carrier does not yet exist"), cell(text: "**emit-generality (continuous)**")]), + row(cells: [cell(text: "**llvm_ir**"), cell(text: "IR/backend"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs)"), cell(text: "bar-c green + frontier row `self-host: N/A (no runtime)` — the Rust/cargo-free lowering path, once a TargetModel is built"), cell(text: "committed TargetModel, configure the `llc`/`clang` runtime row"), cell(text: "**emit-generality (SSA)**")]), + row(cells: [cell(text: "**wasm**"), cell(text: "IR/backend"), cell(text: "has a **TargetModel** (bundle/lex/binding_spellings) BUT **bar-c unreachable** — `runtime_row: target_emit_host_runtime_row_unconfigured` (`v2.extdeps.languages.wasm` `wasm_target_model`)"), cell(text: "bar-c green + frontier row `self-host: N/A` — **blocked on configuring the runtime row**"), cell(text: "configure the `wasmtime` runtime row"), cell(text: "emit-generality (stack machine)")]), + row(cells: [cell(text: "**machine_code / ptx**"), cell(text: "ISA/GPU"), cell(text: "**below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs)"), cell(text: "bar-c green + frontier row `self-host: N/A`, once a TargetModel is built"), cell(text: "committed TargetModel, configure the assembler/`ptxas` runtime row"), cell(text: "emit-generality (ISA)")]), ], }, hr(), h2(text: "Sequencing — Rust-as-model, then stress (dependency-ordered)"), ul(items: [ li(text: "**Phase A — now-ish (pre-un-shelve):** this map + the `solve` rationale. No emit code. ← *we are here*"), - li(text: "**Phase B — foundation de-fork (the barrier; everything downstream inherits):** F4 exe-identity de-fork (row-bound identity + generic dispatch) + F7 decl-emission de-fork (`emit_semantic_decl.dag`) + F2 VEP completion (rust + TS). Once B lands, C/D/E run largely in parallel."), + li(text: "**Phase B — foundation completion (the barrier; everything downstream inherits):** F2 VEP completion (rust + TS). Once B lands, C/D/E run largely in parallel."), li(text: "**Phase C — self-host axis proof:** generalize F5 past Rust to **Go** (first non-Rust self-host) — and land Rust's own self-host (0/27 today). This is the real \"does the seed-shrink story generalize\" milestone. If it holds, java/kotlin/swift are near-mechanical parallel fan-out."), li(text: "**Phase D — emit-generality axis (parallel):** Verilog · SPICE · LLVM-IR to bar-c + frontier rows. Verilog and LLVM-IR first need a **committed TargetModel** (both below bar-a today); SPICE needs its witness to actually run ngspice (bar-b → bar-c). Each decomposes its `body_lexeme:String` scars and binds its simulator/toolchain transport in a row. This is where the design gets *stressed*; a construct that won't lower produces a typed, located refusal that *names the design gap* — the refusal is the product."), li(text: "**Phase E — interpreted self-host:** TS → Python (Python inherits TS's VEP completion)."), @@ -75,7 +74,7 @@ fn language_target_self_host_frontier_body() -> List { p(text: "Each language is **priced by the design risk it displaces**, not by completeness (§6): Verilog=concurrent, SPICE=continuous, LLVM=SSA/self-host-boundary, Lean=expression-spine. A confirm-only language (java/kotlin/swift) earns its slot only as cheap parallel fan-out after its family's proof lands."), hr(), h2(text: "Staffing note (for continuous dispatch)"), - p(text: "Off this map, the natural fan-out is **one child session per language axis**, gated on Phase B. The dependency structure that makes this safe: **B is the only hard barrier** (F4 + F7 de-forks + F2 completion); after it, the self-host axis (C, then the compiled fan-out) and the emit-generality axis (D) have no cross-dependency, so they staff independently. Lean (F) and the interpreted family (E) each ride one Phase-B deliverable (F3-expression-mode and F2-completion respectively) plus their own missing TargetModel where noted. ecmascript's adopt-or-delete decision is a prerequisite gate on the interpreted family, not parallel work."), + p(text: "Off this map, the natural fan-out is **one child session per language axis**, gated on Phase B. The dependency structure that makes this safe: **B is the only hard barrier** (F2 completion); after it, the self-host axis (C, then the compiled fan-out) and the emit-generality axis (D) have no cross-dependency, so they staff independently. Lean (F) and the interpreted family (E) each ride one Phase-B deliverable (F3-expression-mode and F2-completion respectively) plus their own missing TargetModel where noted. ecmascript's adopt-or-delete decision is a prerequisite gate on the interpreted family, not parallel work."), ] } diff --git a/dag/gunbc/plans/typescript_gap_census.dag b/dag/gunbc/plans/typescript_gap_census.dag index 7b45a72bec9..7c986503944 100644 --- a/dag/gunbc/plans/typescript_gap_census.dag +++ b/dag/gunbc/plans/typescript_gap_census.dag @@ -31,8 +31,8 @@ fn typescript_gap_census_body() -> List { li(text: "**#6 enum / disj union** — VEP. Witness: `ts_enum_union_emit_by_execution_exact_holds` (`typescript_enum_union_emit_by_execution_test.dag`)."), li(text: "**#7 module import** — VEP. Witness: `ts_import_emit_by_execution_exact_holds` (`typescript_import_emit_by_execution_test.dag`)."), li(text: "**#8 effect apply** — VEP. Witness: `ts_effect_io_emit_holds` (`typescript_effect_io_emit_test.dag`)."), - li(text: "**#9 fold_call body via translate** — VEP. Witness: `fold_call_closure_emit_keystone_holds` (`fold_call_closure_emit_test.dag`)."), - li(text: "**#10 operators (arith/cmp)** — VEP with **ad-hoc test catalog only** (`add_body_ts_emit_catalog_minus_discriminates`, `add_body_ts_emit_missing_catalog_rejects`). Default `ts_operator_realizations_catalog_node()` enrolls **OpAdd only** (`typescript.dag:640`) — see #16."), + li(text: "**#9 fold_call body via translate** — VEP. Witness: `v2.test.manual.fold_call_closure_emit` `fold_call_emit_holds`; the paired `fold_call_swap_discriminates` is the red control."), + li(text: "**#10 operators (arith/cmp)** — VEP with **ad-hoc test catalog only** (`add_body_ts_emit_catalog_minus_discriminates`, `add_body_ts_emit_missing_catalog_rejects`). Default `v2.extdeps.languages.typescript` `ts_operator_realizations_catalog_node` enrolls **OpAdd only** — see #16."), ]), h3(text: "FAIL-CLOSED (emit explicitly Rejected — named)"), ol(items: [ @@ -41,11 +41,11 @@ fn typescript_gap_census_body() -> List { ]), h3(text: "FAIL-OPEN (compiler-scale; no green bar (b)+(c) on default model today)"), ol(items: [ - li(text: "**#13 match / coproduct dispatch** — `match_form.match_token = ^ts_token_unwired_match` (`typescript.dag:623`); no TS match witness; compiler uses `Match` heavily (`05_eval.dag`)."), - li(text: "**#14 bind-in scoping** — `let_form.in_token = ^ts_token_unwired_bind_in` (`typescript.dag:606`)."), - li(text: "**#15 loop form wiring** — `loop_form.loop_token = ^ts_token_unwired_loop` (`typescript.dag:609`)."), - li(text: "**#16 default operator catalog** — `ts_operator_realizations_catalog_node()` rows = `[ts_add_operator_realization_row()]` only (`typescript.dag:640–641`). Algebra ops miss on default model (`add_body_ts_emit_missing_catalog_rejects`)."), - li(text: "**#17 grammar-inverse rows beyond add** — committed `ts_translation_rules_node()` has **1** child (`fn_add`); witness bundle `ts_translation_rules_witness()` expects **3** (add + type_alias + pr3) (`typescript.dag:1381–1414`)."), + li(text: "**#13 match / coproduct dispatch** — `match_form.match_token = ^ts_token_unwired_match` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`); no TS match witness; compiler uses `Match` heavily (`05_eval.dag`)."), + li(text: "**#14 bind-in scoping** — `let_form.in_token = ^ts_token_unwired_bind_in` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`)."), + li(text: "**#15 loop form wiring** — `loop_form.loop_token = ^ts_token_unwired_loop` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`)."), + li(text: "**#16 default operator catalog** — `v2.extdeps.languages.typescript` `ts_operator_realizations_catalog_node` rows = `[ts_add_operator_realization_row()]` only. Algebra ops miss on default model (`add_body_ts_emit_missing_catalog_rejects`)."), + li(text: "**#17 grammar-inverse rows beyond add** — committed `v2.extdeps.languages.typescript` `ts_translation_rules_node` has **1** child (`fn_add`); `ts_translation_rules_witness` carries **2** rows (add + type_alias), while `ts_pr3_translation_rules_witness` carries **3** (add + type_alias + pr3). Type_alias and pr3 are witnessed candidates but neither is enrolled in the committed bundle."), li(text: "**#18 branch dispatch** — compiler uses `Branch` (`04_infer` / `05_eval`); zero TS emit witnesses."), li(text: "**#19 tsc-green / emit_host oracle** — §5 spec-without-execution crack. Sole consumer path: `ts_host_transport_descriptor` + `emit_host_gate.dag`. **`typescript_descriptor_node_ts_node_run_add_holds` FAIL** (wet `claim_batch`); **`emit_host_gate_passes` FAIL** (wet). Bar (c) red even for add."), li(text: "**#20 whole `src/v2` → TS** — no module; Route-A tsc analogue not started (terminal slice E)."), @@ -64,7 +64,7 @@ fn typescript_gap_census_body() -> List { ol(items: [ li(text: "**A. Land this census** (this plan) — audit-first record, generated md."), li(text: "**A2. tsc-green oracle REAL on existing VEP-green slices (#19 pulled forward)** — per-construct `tsc` acceptance on #1–#9 before stacking breadth. Converts string-green families into compile-green. Highest-value foundation work."), - li(text: "**B. Cheap row extensions (#17)** — enroll type_alias + pr3 rows into committed `ts_translation_rules_node`; rows only, no new TargetModel surface."), + li(text: "**B. Cheap row extensions (#17)** — enroll the type_alias row from `v2.extdeps.languages.typescript` `ts_translation_rules_witness` and the pr3 row from `ts_pr3_translation_rules_witness` into committed `ts_translation_rules_node`; rows only, no new TargetModel surface."), li(text: "**C. Operator catalog (#16)** — proceed **only** if genuinely row-derivation onto the default model; if it needs a new TargetModel surface → load-bearing → sign first."), li(text: "**D. HOLD for parent sign:** Match (#13) + loop/bind (#14–#15) + Branch (#18) — compiler-scale TargetModel surfaces."), li(text: "**E. Whole-tree Route-A tsc (#20)** — terminal."), diff --git a/docs/plans/cardinality-refinement.md b/docs/plans/cardinality-refinement.md index 9c2bebae2d5..af1f07337ff 100644 --- a/docs/plans/cardinality-refinement.md +++ b/docs/plans/cardinality-refinement.md @@ -2,34 +2,33 @@ **Status:** scoping (Feature-1 from the byte-grounding thread). **DESIGN.md + carriers are authority** (§6 no parallel ledger); each item dissolves into a wired parser/checker change + a green witness when it lands. -**Verified against the live tree 2026-06-22.** Line numbers are receipts; re-check before acting. +**Verified against the live tree 2026-07-31.** Symbols, not line positions, are receipts; re-check the cited declarations before acting. ## 0. Thesis — cardinality is ONE axis, and it is the *decidable* refinement fragment "Is it empty", "does it have N", "did `Int64` overflow" are the same question — a **cardinality constraint** — answered today by scattered manual `if list_length(..) == 0` / `count` / bound checks. Model cardinality as a refinement **axis** and two things fall out: -1. **Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`admits: fn(B) -> Bool`, `refinement.dag:34`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it. +1. **Decidability (why this fragment, not general refinement).** Arbitrary value predicates (`v2.std.refinement` `Validation.admits: fn(B) -> Bool`) are undecidable, so they can only be checked at a runtime constructor boundary. **Cardinality** predicates — `length == N`, `≥ 1`, `magnitude < 2^width` — are linear arithmetic over counts: **decidable**, hence checkable *statically* and fold-propagated. Scoping refinement to cardinality is what keeps it inside the §4 bounded/decidable substrate; general refinement would break it. 2. **Fold-propagation (the payoff).** A catamorphism that carries the cardinality means folding a `List` yields its length, adding two bounded `Int64` yields the combined bound (and **overflow is a typed `Rejected`, not a silent wrap**). "When we fold, it's handled automatically" — the empty/count/width checks stop being hand-written. ## 1. What is ALREADY built (this is wiring, not greenfield) -- **Value-level refinement substrate — `v2.std.refinement`:** `Validation { reason, admits: fn(B)->Bool }`, `Refined { base }`, and `refine(base, by, at) -> Outcome>` (`:74`) which checks `admits(base)` and returns `Accepted{Refined}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements. -- **Its own documented gaps:** `🟡 feature:refinement-opaque-carrier / T-25-tail` (`:65`) — bare `Refined { base }` can still bypass `refine`; construction is **not compiler-enforced** yet. -- **The phantom-width gap — `std.machine_constraints`:** `type MachineWidth` (`:47`) is a phantom; its TRACKED PARAMETER GAP (`:34-46`) names the exact trigger: *"substrate grammar for bounded phantom parameters tying `bits` to `Nat`, or a non-phantom `MachineWidth` indexed by an explicit `Nat` carrier."* No reflection of `N` to a value. -- **The structural carriers exist, unchecked — `std.bit`:** `Byte { bits: List }` (`bit.dag:25`), header concedes *"cardinality is not enforced … no lowered field refinement, type-alias `where` is skipped in the handwritten parser."* -- **A waiting consumer — `std.measure`:** `Refined, predicate>` is explicitly **deferred** (`measure.dag:8,245`), waiting on exactly this. +- **Value-level refinement substrate — `v2.std.refinement`:** `Validation`, `Refined`, and `refine` check `Validation.admits` and return `Accepted{Refined}` / `Rejected` — **fail-closed, already.** Plus hoisted int refinement factories and iteration-ordering refinements. +- **The carrier has not consumed the existing construction wall:** `v2.std.refinement` `Refined` exposes its `base` field and is not marked `sole_constructor`. The compiler already refuses cross-module construction of `sole_constructor` records through `v1.compiler.infer` `type_has_sole_constructor` / `SoleConstructorViolation`; per DESIGN §4b, its completeness for generic refinement carriers, every construction form, and compiler-module exemptions is **unverified**, not absent. +- **The phantom-width gap — `std.machine_constraints` `MachineWidth`:** the declaration has a type parameter but no value carrier. No reflection of `N` to a value exists. +- **The structural carrier exists, unchecked — `std.bit` `Byte`:** its `bits: List` field carries no cardinality refinement. ## 2. The gap, decomposed (each piece → a real surface) -- [ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Parser: extend the type-RHS path (`parse_type_rhs_after_eq`, named in `machine_constraints.dag:109`) and the record-field path to accept `where `; lex the `where` keyword. Normalize: at the `^dag_surface_type_alias_rhs` hook (`03_normalize.dag:90`) lower `where P` into a `Validation` + a **refined-construction obligation** on the type. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression. -- [ ] **P2 — compiler-enforced construction (closes T-25-tail).** Checker: at a construction site of a refined type, require the obligation discharged — bare `Byte { bits: … }` outside the sanctioned `refine`/smart-constructor is a located `Rejected`, never silent. This is what turns "documented intent" into "illegal-state-unwritable." -- [ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length` (`== N`), `NonEmpty` (`≥ 1`), `Bounded`, `Width` (the `MachineWidth` bound). All are linear-arithmetic over `list_length` (`types.dag:233`) / magnitude — decidable. `Byte = { bits: List } where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.** +- [ ] **P1 — surface `where` syntax, desugaring to `refine`/`Validation`.** Extend `v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr` and the record-field grammar to accept `where `. Register the emitted surface form through `v2.std.compilers.sugar` and lower it through `v2.compiler.normalize` `normalize_sugar_key_optional` into a `Validation` + a **refined-construction obligation**. MVP = alias/field-level `where`; the predicate is from the closed cardinality vocabulary (P3), not an arbitrary expression. +- [ ] **P2 — audit and consume the existing construction wall (closes T-25-tail).** First run discriminating positive/negative probes for `sole_constructor` on generic `Refined`, every record-construction form, and the compiler-module exemptions named by DESIGN §4b. If that audit is complete, mark the canonical refinement carrier and route sanctioned construction through `refine`/its smart constructor; if a probe escapes, extend the existing wall at that measured gap rather than minting a parallel checker. The required outcome is that bare refined construction outside the sanctioned factory produces a located `SoleConstructorViolation`, never silent acceptance. +- [ ] **P3 — the closed cardinality predicate vocabulary (the decidable fragment).** A small closed set grounded in `Validation.admits`: `Length` (`== N`), `NonEmpty` (`≥ 1`), `Bounded`, `Width` (the `MachineWidth` bound). All are linear-arithmetic over `std.types` `list_length` / magnitude — decidable. `Byte = { bits: List } where Length<8>`; `Int64`'s magnitude is `Bounded<0, 2^64>`. **No arbitrary predicate enters static checking.** - [ ] **P4 — fold-propagation (the novel, high-value piece).** Extend the catamorphism (`fold_node` / the reduce) so a cardinality fact is COMPUTED through a fold: `Cons/Empty` over a list yields its length; combining two `Bounded` magnitudes yields the combined bound, and a bound exceeding the `Width` is a typed overflow `Rejected`. Connect to the existing cost-through-folds algebra (`induction.dag` PolyCost/exponents) — cardinality is the same shape (a count tracked through a catamorphism) as the cost lens already computes. -- [ ] **P5 (stretch) — type-level-Nat reflection.** Reflect `MachineWidth`'s `N` to a value (the phantom→value bridge named in `machine_constraints.dag:43-46`), so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal. +- [ ] **P5 (stretch) — type-level-Nat reflection.** Add the value bridge absent from `std.machine_constraints` `MachineWidth`, so `bits_per_byte` dissolves into `width(Byte)` and `Int64`'s bound derives from its type rather than a literal. ## 3. Where it plugs into the pipeline -`tokenize` (lex `where`) → `parse` (`parse_type_rhs_after_eq`: parse the cardinality pred, attach to the type-decl `Node`) → `normalize` (`dag_surface_type_alias_rhs`: desugar to `Validation` + the construction obligation) → `infer` (`04_infer`: discharge the obligation at construction sites — the decidable cardinality check — and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time). +`tokenize` (lex `where`) → `parse` (`v2.extdeps.languages.dag` `dag_grammar_type_alias_rhs_expr`: attach the cardinality predicate to an emitted surface node) → `normalize` (`v2.compiler.normalize` `normalize_sugar_key_optional`: desugar through the sugar registry to `Validation` + the construction obligation) → `infer` (discharge the obligation at construction sites and fold-propagate cardinality facts) → `emit` (refinements erase, or ground to a target assert; they are compile-time). ## 4. The decidability boundary (the one rule that keeps this §4-legal) @@ -47,14 +46,14 @@ Two tiers, and the split is the whole discipline: ## 6. What one feature unblocks (the ROI) -Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; `Measure` inhabitance (the deferred `Refined`); typed `|>` coercion (the Measure-inhabitance gap blocked it last week); `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings. +Byte=8bits; the scattered empty/count/length checks → cardinality facts; `Int64` overflow → a bound through the fold; typed `|>` coercion; `NonEmptyStr`/`NonEmptyDiagnostics` → `NonEmpty`. One axis, many groundings. ## 7. Risks / hard parts - **Decidability discipline** (§4) — the failure mode is P3/P4 quietly admitting a non-cardinality predicate; gate it to the closed vocabulary. - **Fold-propagation soundness** — the cardinality a fold computes must be *provably* the real one (a fail-closed witness: a fold that miscounts goes RED). -- **The parser is handwritten** (`bit.dag` header) — `where` lexing/parsing touches the seed parser (load-bearing; sequence behind the §0 lock-down, not during it). -- **P2 is broad** — construction-enforcement touches every construction site of a refined type. +- **The parser/normalizer path is load-bearing** — `where` must enter through the modeled grammar and sugar registry, sequenced behind the §0 lock-down. +- **P2 completeness is unverified** — audit the existing `sole_constructor` wall across generic carriers, every construction form, and compiler-module exemptions before declaring the attainable ceiling or extending enforcement. ## Dissolution trigger (DESIGN §6) diff --git a/docs/plans/compile-clean-forcecheck.md b/docs/plans/compile-clean-forcecheck.md index e925e6d42fa..cc3d53ea6b2 100644 --- a/docs/plans/compile-clean-forcecheck.md +++ b/docs/plans/compile-clean-forcecheck.md @@ -1,16 +1,16 @@ # Plan — compile-clean gate force-check (ROADMAP §1 floor-coverage / §0 inference fail-open) -**Status:** diagnosis (done, execution-proven) + **(A) partition design** + **blast-radius measured (10 names / 102 sites)**. Scope confirmed by parent `quick-ant-298`: **DESIGN-FIRST + MEASURE-FIRST, land nothing enforcing** — the tree-scoping/registry-partition *flip* is operator-gated (escalates via parent + bright-stag). **DESIGN §5 (fail-closed) is authority.** Work-item `adhoc-6169238c-5e2`. Linked from `ROADMAP.md §0` (line 31, "inference fail-open — return-type after #5293") and §1 (floor-coverage). Sibling of [fail-closed-lockdown.md](fail-closed-lockdown.md) §3 (where the pipeline fails open). Adjacent: 2(i) (bright-stag `adhoc-8e5771e1-14a`) grounds `utf8_decode_bytes` as a real std fn — **(A) is what makes such grounding required by construction** so the leak can't recur. +**Status:** historical diagnosis (execution-proven) + live **(A) partition design**. The 10-name / 102-site blast radius is a 2026-06-21 capture, not a live census. **DESIGN §5 (fail-closed) is authority.** Sibling of [fail-closed-lockdown.md](fail-closed-lockdown.md) §3. -**Verified against the live tree 2026-06-21** — `gunbc` built from `src/v1/stage0`, probes + the empty-registry blast-radius compile run. Line numbers are receipts. +**Re-verified against the live tree 2026-07-31.** `v1.compiler.infer_method` `builtin_function_registry` remains a flat global name→type map; `std.encoding` `utf8_decode_bytes` is now grounded and its old registry row is gone. Symbols, not line positions, are receipts. ## 0. Verdict — the brief's mechanism is wrong; the leak is a global seed allowlist -The compile-clean gate (`dag/tools/dag_compile_clean_gate.dag` → `gunbc compile --target rust` over `dag/` with `src/v2` as the import pool) is **fail-open**: `gunbc compile` on `main` returns 0 diagnostics / EXIT 0 even though `dag/extdeps/cloud/gcp/secret_manager.dag:71` calls `utf8_decode_bytes`, which is **defined nowhere in `dag/` or `src/v2`**. +At the 2026-06-21 capture, the compile-clean gate (`dag/tools/dag_compile_clean_gate.dag` → `gunbc compile --target rust` over `dag/` with `src/v2` as the import pool) was **fail-open**: `gunbc compile` on `main` returned 0 diagnostics / EXIT 0 even though `extdeps.cloud.gcp.secret_manager` `utf8_secret_from_access_payload` called `utf8_decode_bytes`, which was then **defined nowhere in `dag/` or `src/v2`**. The current tree now defines `std.encoding` `utf8_decode_bytes`; this paragraph is a historical execution receipt, not a claim that the literal leak remains live. -The brief framed this as "unreached fn bodies escape typecheck." **That is false** — bodies are always visited. The precise mechanism (execution-proven, §1 below) is two independent fail-open holes: +The brief framed this as "unreached fn bodies escape typecheck." **That was false** — bodies were always visited. At the captured run, the execution-proven mechanism (§1 below) was two independent fail-open holes: -1. **Registry leak** — `utf8_decode_bytes` resolves because it is a hardcoded entry in the global `builtin_function_registry()`, an **explicitly-marked BRIDGE scaffold**. The registry is *not scoped to the tree being compiled*, so v1-seed runtime intrinsics leak into the dag-substrate compile. +1. **Registry leak at capture** — `utf8_decode_bytes` resolved because it was a hardcoded entry in the global `builtin_function_registry()`, then an **explicitly-marked BRIDGE scaffold**. The registry was *not scoped to the tree being compiled*, so v1-seed runtime intrinsics leaked into the dag-substrate compile. 2. **Return-type fail-open** — a function whose body's inferred type ≠ its declared return type is not flagged (`#5293` closed only the record-field hole, not return types). Independent of the gate; a member of ROADMAP §0's "inference fail-open (return-type after #5293)". ## 1. Execution-proven mechanism (receipts) @@ -24,7 +24,7 @@ The brief framed this as "unreached fn bodies escape typecheck." **That is false | call to **registered** seed builtin | `fn f()->Int{ utf8_decode_bytes(payload:3) }` | **0 diagnostics** | registry absorbs the name → `string_type`, no def required, no arg check | | plain return-type mismatch | `fn f()->Int{ "a string" }` | **0 diagnostics** | declared return type unenforced | -**The real on-main witness** — `dag/extdeps/cloud/gcp/secret_manager.dag:70-72`: +**The real on-main witness** — `extdeps.cloud.gcp.secret_manager` `utf8_secret_from_access_payload`: ``` fn utf8_secret_from_access_payload(payload: Bytes) -> Secret { @@ -32,36 +32,32 @@ fn utf8_secret_from_access_payload(payload: Bytes) -> Secret { } ``` -`utf8_decode_bytes` resolves via the registry; the `as Secret` cast satisfies the return type. So the **literal witness is hole #1 alone** (return-type enforcement would not catch it because of the cast). +In the captured run, `utf8_decode_bytes` resolved via the registry; the `as Secret` cast satisfied the return type. So the **literal witness was hole #1 alone** (return-type enforcement would not have caught it because of the cast). ## 2. The seam — `builtin_function_registry` -`src/v1/04_method.dag:55-155` (Rust seed `v1_compiler_infer_method.rs:100-365`). 76 names → return-type `Node`s, e.g. `utf8_decode_bytes → string_type` (04_method.dag:93). Its own header is the indictment: +At capture, `v1.compiler.infer_method` `builtin_function_registry` held 76 names → return-type `Node`s, including a `utf8_decode_bytes → string_type` row. That row is absent now, but the live registry remains a flat global map. `std.encoding` `utf8_decode_bytes_host_realization_marker` and `std.bytes` `bytes_seam_host_realization_marker` exist, but both carry a stale `DeclarationRef` to `std.bytes` `builtin_function_registry`, where no such declaration exists. They are unresolved scaffold debt, not verified bindings to the live v1 registry. -> `// BRIDGE: This map_insert chain is a duplicate authority over facts that should come from .dag` -> `// function declarations (extern fn signatures). Deletion point: when builtins are actual .dag` -> `// definitions that the compiler loads and resolves, this registry is deleted.` +The flat live registry remains a known §3 fork (duplicate authority); the two broken marker references are a second §3 gap that must repair or dissolve with it. Two registry properties make the resolution seam fail-open: -So this is a known §3 fork (duplicate authority) with a **named dissolution trigger**. Two properties make it the fail-open: - -- **Global, not tree-scoped.** The same registry is consulted whether the entry root is `src/v1` (the seed, which legitimately needs `utf8_decode_bytes`/`scan_while`/… as its runtime kernel — used in `05_emit_rust.dag`, `runtime_rust.dag`) or `dag/` (the substrate, which must not depend on seed intrinsics). A name in the registry resolves in *any* tree. +- **Global, not tree-scoped.** The same registry is consulted whether the entry root is `src/v1` (the seed, which legitimately needs seed-only intrinsics such as `scan_while`) or `dag/` (the substrate, which must not depend on seed intrinsics). A name in the registry resolves in *any* tree. - **Resolution without definition or arg-check.** A registry hit yields a fabricated return type with no parameter typing and no requirement that a definition exist in the compiled closure — DESIGN §5's "fabricated plausible output" anti-pattern, at the call-head resolution seam. -(`resolve_builtin_call_type`'s `Absent => unit_type`, 04_method.dag:166, is *not* a live leak for call syntax — unregistered names are caught upstream as "function not found in scope". It is a latent fail-open kept for non-call uses; out of scope here, noted for the audit.) +(`v1.compiler.infer_method` `resolve_builtin_call_type`'s `Absent => unit_type` is *not* a live leak for call syntax — unregistered names are caught upstream as "function not found in scope". It is a latent fail-open kept for non-call uses; out of scope here, noted for the audit.) ## 3. Construction-correct direction (DESIGN §5/§3) -The gate's claim is "the dag substrate is well-typed **and self-contained**." Made *unwritable* (§5 construction, not a post-hoc lens): **the set of resolvable builtins must be derived from the tree being compiled, not a global seed allowlist.** This is exactly the registry's own stated deletion point — builtins become real `.dag` definitions resolved through normal import/definition resolution, the global registry is deleted, and a substrate that neither defines nor imports `utf8_decode_bytes` fails closed on it ("function not found in scope", identical to probe 2). At that point the leak is dead by construction, not by a roster. +The gate's claim is "the dag substrate is well-typed **and self-contained**." Made *unwritable* (§5 construction, not a post-hoc lens): **the set of resolvable builtins must be derived from the tree being compiled, not a global seed allowlist.** This is exactly the registry's own stated deletion point — builtins become real `.dag` definitions resolved through normal import/definition resolution, the global registry is deleted, and a substrate that neither defines nor imports a live seed-only name such as `scan_while` fails closed on it ("function not found in scope", identical to probe 2). At that point the leak is dead by construction, not by a roster. -Full dissolution (76 builtins → `.dag` defs) is a large migration, out of this node's scope. The bounded options below are stepping stones; (A) is the one that closes the literal witness *by construction*. +Full dissolution of the flat registry into `.dag` definitions is a large migration, out of this node's scope. The bounded options below are stepping stones; (A) closes the leak class *by construction*. ## 4. Scope decision (parent-confirmed) — (A), as design + measure only Parent `quick-ant-298` confirmed: this node ships **(A)'s design + the blast-radius measurement**, and **lands nothing enforcing**. (B) and (C) are split out: -- **(A) Tree-scoped builtin availability / registry partition** — the direction. Split the registry into *substrate-available* builtins (real `.dag`/std defs, or the sanctioned primitive surface) and *seed-only kernel* intrinsics; admit the seed-only set only when the entry root is the v1 seed itself. A dag-substrate compile then fails closed on a seed-only name. This **advances the registry's own marked dissolve-on** (04_method.dag:55-62) — it is not new debt. The enforcing flip is **load-bearing** (inference scope) + **changes what compiles** → operator-gated; escalates via parent + bright-stag. This doc + §6's measured number is the input to that sign-off. -- **(B) Return-type enforcement** — SEPARATE (ROADMAP §0 line 31; #5293 closed only record-field). Does not close the literal witness (the `as Secret` cast satisfies the return type). Its own PR later. Flagged adjacent, not bundled. -- **(C) Grounding `utf8_decode_bytes` as a real std fn** — **2(i)'s job** (bright-stag `adhoc-8e5771e1-14a`). Nuance relayed: `utf8_decode_bytes` is a *registry entry* (→ `string_type`), not purely undefined — so 2(i) must define the std fn **and** delete its registry bridge row, else the registry shadows the new def. (A) is what makes that grounding *required* by construction. +- **(A) Tree-scoped builtin availability / registry partition** — the live direction. Split the registry into *substrate-available* builtins (real `.dag`/std defs, or the sanctioned primitive surface) and *seed-only kernel* intrinsics; admit the seed-only set only when the entry root is the v1 seed itself. A dag-substrate compile then fails closed on a seed-only name. The enforcing flip is **load-bearing** (inference scope) + **changes what compiles** → operator-gated; it must also repair or dissolve the stale marker `DeclarationRef`s rather than treating them as authority. +- **(B) Return-type enforcement** — separate. It did not close the historical literal witness because the `as Secret` cast satisfied the return type; do not bundle it with registry partitioning. +- **(C) Grounding `utf8_decode_bytes` as a real std fn — complete.** `std.encoding` now declares `utf8_decode_bytes`, and the historical registry row is gone. Its host realization still carries `utf8_decode_bytes_host_realization_marker`, which dissolves with the registry fork. ## 5. (A) partition design @@ -72,7 +68,7 @@ Parent `quick-ant-298` confirmed: this node ships **(A)'s design + the blast-rad **Construction shape (the registry's dissolve-on, staged):** each builtin row carries an **availability tag** — `SubstrateAvailable` vs `SeedOnly` — instead of a flat name→type map. The call-head resolver admits a `SeedOnly` row **only when the compile's entry root is the v1 seed**; for a substrate entry root (dag/ + v2 pool) a `SeedOnly` hit is treated as *not a builtin* → falls through to the existing fail-closed "function not found in scope" (probe 2). `SubstrateAvailable` rows are the sanctioned primitive surface and, per the dissolve-on, migrate to real `std` `.dag` defs over time; once a name has a real def it leaves the registry entirely and resolves through normal func-env lookup. -- *Entry-root signal*: the existing entry-vs-pool distinction (`main.rs:343-347` "entry modules = all .dag in the FIRST source root; additional roots are dependency pools") already separates the compiled tree from its pools. The infer scope must carry one bit — "entry root is the v1 seed" — derived from whether `src/v1` is the primary `--source-root`. (Threading this into `InferScope` is the load-bearing part; out of scope for this node — captured here for the enforce PR.) +- *Entry-root signal*: the existing entry-vs-pool distinction (`v1.compiler.emit_rust` `emit_compile_match_arm`: "entry modules = all .dag in the FIRST source root; additional roots are dependency pools") already separates the compiled tree from its pools. The infer scope must carry one bit — "entry root is the v1 seed" — derived from whether `src/v1` is the primary `--source-root`. (Threading this into `InferScope` is the load-bearing part; out of scope for this node — captured here for the enforce PR.) - *Why a tag, not a second map*: a second allowlist map would be a new parallel authority (§3). One row per builtin with an availability field keeps single authority and reads as construction, not a lens. - *Non-enforcing intermediate (this node)*: the empty-registry measurement in §6 already enumerates the exact leak set without any code change shipping. The enforce PR turns each `SeedOnly` substrate hit into the fail-closed path behind operator sign-off. @@ -91,16 +87,16 @@ Result: **102 diagnostics, all "not found in scope", 10 distinct names** (all in | `set_contains` | 3 | dag/std | set primitive | | `set_insert` | 2 | dag/std | set primitive | | `count` | 2 | dag/gunbc/tools | general primitive | -| `utf8_decode_bytes` | 1 | **dag/extdeps/cloud/gcp** | **the brief's witness — true domain leak (2(i) grounds it)** | +| `utf8_decode_bytes` | 1 | **dag/extdeps/cloud/gcp** | **historical brief witness — domain leak later grounded under completed (C)** | | `hash_combine` | 1 | dag/std | hashing primitive | | `atom_identity_hash` | 1 | dag/std | hashing primitive | -**Reading of the number:** the (A) rollout is **small and tractable**, not a corpus-wide flag day. 8 of the 10 (96 sites) are the accepted general-purpose primitive surface (`string_contains`, `to_string`, `concat`, `count`, `set_contains`, `set_insert`, `hash_combine`, `atom_identity_hash`) — these become `SubstrateAvailable` and are the std-grounding backlog. `filesystem_read` (5) is the already-known lens reflection fork. Exactly **one** name — `utf8_decode_bytes` — is a genuine domain leak, and it is already owned by 2(i). So (A) tags 8–9 substrate primitives + the lens-reflection intrinsic, and the only domain code that fails closed under (A) today is the single gcp site, which 2(i) is already grounding. The blast radius gates the rollout: tag the 8 primitives `SubstrateAvailable` first (no breakage), then flip seed-only enforcement once `utf8_decode_bytes` is grounded. +**Reading of the captured number:** on 2026-06-21, 8 of the 10 names (96 sites) were general-purpose primitive calls (`string_contains`, `to_string`, `concat`, `count`, `set_contains`, `set_insert`, `hash_combine`, `atom_identity_hash`), `filesystem_read` (5) was the known lens-reflection fork, and `utf8_decode_bytes` (1) was the sole domain leak. Completed (C) has since grounded `std.encoding` `utf8_decode_bytes` and removed its registry row, so this capture does **not** identify a live domain-code failure or establish today's rollout size. Before enforcing (A), re-run the real compile measurement against the current registry, classify each remaining live row as `SubstrateAvailable` or `SeedOnly`, then prove the partition with the `scan_while` red in §7. ## 7. Discriminating witness (must go RED when the behavior is wrong) -The enforce PR's receipt is the same shape as §6's method: a planted substrate module that free-calls a `SeedOnly` builtin (`utf8_decode_bytes`) must make `gunbc compile` over the dag pools **fail**; the identical module compiled with the `src/v1` seed as primary root must **pass**. Green-by-execution against the real `gunbc`, not a typecheck/grep. (DESIGN §5: spec-without-execution is not done.) +The enforce PR's receipt is the same shape as §6's method: a planted substrate module that free-calls a live seed-only builtin such as `scan_while` must make `gunbc compile` over the dag pools **fail**; the identical call compiled under the `src/v1` seed must **pass**. Green-by-execution against the real `gunbc`, not a typecheck/grep. (DESIGN §5: spec-without-execution is not done.) ## Dissolution trigger (DESIGN §6) -Delete this doc when (A) lands as construction: the builtin registry carries a `SubstrateAvailable`/`SeedOnly` availability tag, a dag-substrate compile fails closed on a seed-only name (the §7 discriminating witness green-by-execution — a planted `utf8_decode_bytes` call fails over the dag pools and passes under the v1-seed root), and `utf8_decode_bytes` is grounded as a real std def with its registry bridge row deleted — at which point the leak is dead by construction (DESIGN §5), the registry's own marked dissolve-on (04_method.dag:55-62) has advanced, and this design+measurement doc is superseded by the wall it specified. +Delete this doc when (A) lands as construction: the builtin registry carries a `SubstrateAvailable`/`SeedOnly` availability tag, a dag-substrate compile fails closed on a live seed-only name such as `scan_while` while the v1 seed admits it, and the stale `DeclarationRef`s in `utf8_decode_bytes_host_realization_marker` / `bytes_seam_host_realization_marker` are repaired onto a live authority or dissolve — at which point the leak is dead by construction (DESIGN §5). diff --git a/docs/plans/format-model-reconciliation.md b/docs/plans/format-model-reconciliation.md index 5197d7e7fb6..3a0b4d44c76 100644 --- a/docs/plans/format-model-reconciliation.md +++ b/docs/plans/format-model-reconciliation.md @@ -1,31 +1,31 @@ # Format-model reconciliation — record spelling onto single authority -> Record-spelling reconciliation: one concept — how a format spells records — was forked across three models, and no text format routes serialization through any of them today. DESIGN refs: §2 (one concept every scale — decompress the leaf, map to existing carriers, reduce duplicates), §3 (single authority — field-by-field decomposition onto ConfigFormat, CommentSyntax, LayoutProtocol; delete uninhabited scaffolds), §5 (construction over validation — the swap test is execution-grounded), §6 (complementary to [regime-2 shared emission fold](regime2-shared-emission-fold.md), not a parallel ledger). +> Record-spelling reconciliation: one concept — how a format spells records — was historically forked across three models. The live tree has dissolved the two legacy models into `ConfigFormat`, `CommentSyntax`, `LayoutProtocol`, and `SerializationKnobs`; this tracker now owns only the remaining emitter migrations. DESIGN refs: §2 (one concept every scale), §3 (single authority), §5 (execution-grounded swap test), §6 (complementary to [regime-2 shared emission fold](regime2-shared-emission-fold.md), not a parallel ledger). -**Status:** planning tracker · **`.dag` carrier is authority** (§6). Linked from `ROADMAP.md` §6 cross-media band. Carrier facts verified against the live tree 2026-06-30. **Code keystone:** still-wolf-292 / PR #6045 (C1) — this doc captures only; no serializer code here. +**Status:** implementation tail · **`.dag` carrier is authority** (§6). Carrier facts re-verified against the live tree 2026-07-31. -## 1. The fork — three models, zero routed serializers +## 1. The historical fork and its live resolution Layout (line/indent/newline) is [regime-2 shared emission fold](regime2-shared-emission-fold.md). **This doc owns record spelling** — how key/value, assign, quoting, and nesting render into text or JSON: | model | where | role | verdict | | --- | --- | --- | --- | -| `ConfigFormat` | `dag/std/languages.dag` | format **identity** (id, name, extensions, comment) | **keep** | -| `FormatModel` | `dag/std/languages.dag:36` | indent, max_line_width, import_grouping, trailing_newline | **uninhabited dead scaffold** — delete | -| `OutputFormat` | `dag/std/render.dag:160` | name, indent_unit, kv_separator, list_prefix, comment_prefix, section_separator, trailing_newline | **only live knob record** — sole consumer `gitignore_output_format`; `comment_prefix` is a §3 nickname of `CommentSyntax.line_prefix` | +| `ConfigFormat` | `std.languages` `ConfigFormat` | format identity plus optional record knobs | **live authority** | +| `FormatModel` | absent from the live tree | legacy layout scaffold | **deleted** | +| `OutputFormat` | absent from the live tree | legacy mixed layout/record knobs | **deleted and decomposed** | -No text format today routes record serialization through any of these types — emitters hand-roll `concat` / `match` per site. +`std.languages` `SerializationKnobs` and `std.serialize` `serialize_record_doc` now carry record spelling. `gunbc.runner_deploy_emit` routes manifest and JSON projections through them; remaining boutique emitters are scoped below. ## 2. The decomposition — map each field to its single authority (§3) -Decompose `OutputFormat` field-by-field onto existing carriers; the irreducible residue is the record-spelling knobs only: +The deleted `OutputFormat` was decomposed field-by-field onto existing carriers; the irreducible residue is the record-spelling knobs only: - `name` → `ConfigFormat` (identity already lives there) - `comment_prefix` → `CommentSyntax.line_prefix` (derive `#` from format comment, never duplicate) - `indent_unit`, `trailing_newline` → `std.layout.LayoutProtocol` (line-layout half; owned by regime-2) - **Residue → `SerializationKnobs`** in `std.languages`: assign separator, entry separator, open/close delimiters, quoting policy — a comment-free record-spelling value -**Target pipeline:** a total `serialize_record` fold producing `std.layout.Doc` (recursive — JSON/proto nesting fits). Compose with regime-2 `render(doc, protocol)` for the line half. +**Live pipeline:** `std.serialize` `serialize_record_doc` produces `std.layout` `Doc` recursively; compose it with `std.layout` `render` for the line half. ``` doc = serialize_record(record, knobs) // record half (this doc) @@ -34,39 +34,39 @@ text = render(doc, layout_protocol) // line half (regime-2) ### The swap test (acid test) -The **same** record projection renders as manifest text **and** JSON by swapping only the `SerializationKnobs` value — one `serialize_record`, two knob instances, byte-identical witnesses. This is the substrate that makes JSON-as-first-class real under §6 cross-media. +`test.claim.config_record_emit_witness` and `test.claim.runner_placement_witness` exercise the same record projection with manifest and JSON knob values. This is the execution-grounded substrate for JSON-as-first-class under §6 cross-media. ### Relationship to regime-2 (complementary, not duplicate) - [regime-2 shared emission fold](regime2-shared-emission-fold.md) — **line-layout half**: one `render(doc, protocol)` fold over `std.layout.Doc` for yaml/gitignore/runner-deploy/ci.yml projections. - **This doc — record-spelling half**: `serialize_record` → `Doc`, then regime-2 renders. Cross-reference only; do not merge the plans. -## 3. Hazard — do not build on `std.render` kv helpers +## 3. Boundary — `std.render` kv helpers are presentation utilities -`std.render` `kv_pair` / `kv_block` are **broken** for real emission: in `.dag` runtime literals bare curly-brace interpolation is live, while the escaped-brace form in `render.dag:119-120` emits literal brace characters, not key=value pairs. `digest_render.dag` and friends must route through `serialize_record`, not these helpers. +`std.render` `kv_pair` and `kv_block` correctly render caller-supplied separators, but they do not carry format-owned `SerializationKnobs` or recursive record structure. Keep them for presentation-only key/value lists; record emitters such as manifest and JSON projections route through `std.serialize` `serialize_record_doc`. -## 4. Ordered scope (C1–C6) +## 4. Ordered scope (completed foundation, then remaining tail) -1. **C1 (keystone — still-wolf-292 / PR #6045):** `SerializationKnobs` residue in `std.languages` + recursive `serialize_record` → `Doc` + delete `FormatModel`; migrate runner manifest (`dag/gunbc/runner_deploy_emit.dag` — `manifest_host_text` / `session_host_text` / `operating_row_text`) byte-identically; JSON knobs instance + swap-test witness. -2. **C2 (folded into C1):** runner manifest + JSON as the first proving instance — not a separate roadmap row. -3. **C3:** gitignore de-fork — migrate live `OutputFormat` consumer (`dag/gunbc/gitignore_emit.dag` + `extdeps/git/gitignore.dag`) onto `SerializationKnobs` + `ConfigFormat`, derive `#` via `CommentSyntax`, then **delete `OutputFormat`** and orphan `extdeps/git/gitignore_render.dag` (declares knobs then ignores them). -4. **C4:** dnsmasq emit — add dnsmasq `ConfigFormat` + knobs; keep cited positional micro-syntax honest (do not force pure key=value). -5. **C5 (low):** digest/accelerator kv blocks (`dag/gunbc/digest_render.dag` and friends) — route through `serialize_record`; supersedes broken `std.render` kv helpers. -6. **C6 (cosmetic):** CSS declaration blocks — `dag/gunbc/roadmap_style.dag` `css_rule(selector, props)` has `props` as raw `String` (`css_rule_props_scaffold`); flat `property:value` records (assign `: `, separator `; `) are `serialize_record` candidates; selector nesting stays structural. Plus yaml/markdown/html identity-link cosmetics. +1. **C1 complete:** `std.languages` `SerializationKnobs` + recursive `std.serialize` `serialize_record_doc` → `Doc`; `FormatModel` deleted; `gunbc.runner_deploy_emit` manifest fields migrated byte-identically. +2. **C2 complete (folded into C1):** runner manifest + JSON are the first proving instance, witnessed by `test.claim.config_record_emit_witness` and `test.claim.runner_placement_witness`. +3. **C3 complete:** `OutputFormat` and the orphan gitignore renderer are absent. `gunbc.gitignore_emit` derives comments from `std.languages` `gitignore_format` and renders a `Doc` with its `gitignore_protocol`; because gitignore is a line-list rather than a record, it does not acquire fake `SerializationKnobs`. +4. **C4 complete at the honest boundary:** `extdeps.formats.dnsmasq` projects directives to `Doc` with `dnsmasq_protocol`; its positional micro-syntax remains explicit rather than being forced into a key/value record. +5. **C5 (low):** classify digest/accelerator key/value blocks (`gunbc.digest_render` and `gunbc.accelerator_demo_render`) by semantic grain: presentation-only lists stay on the correct `std.render` helpers; true record projections route through `std.serialize` `serialize_record_doc` with byte-identical witnesses. +6. **C6 complete:** `gunbc.roadmap_style` now uses typed `CssDecl` rows on shared `BuildRule` machinery; the old `css_rule_props_scaffold` remains only as historical text in its dissolution note. -## 5. Audit receipts (live tree 2026-06-30) +## 5. Audit receipts (live tree 2026-07-31) -- `FormatModel` at `languages.dag:36` — type only, zero `data` rows, not in `LanguageSpec`. -- `OutputFormat` at `render.dag:160` — consumed by `extdeps/git/gitignore.dag` `gitignore_output_format` only. -- `extdeps/git/gitignore_render.dag` — orphan knob declarations, ignored at emit. -- `languages_consumer_census` baselines: 71 total decls, 64 language rows, 7 format rows (`src/v2/lens/languages_consumer_census.dag:9-11`). +- No `FormatModel`, `OutputFormat`, `gitignore_output_format`, or `gitignore_render` declaration remains in the live tree. +- `std.languages` `ConfigFormat.record` carries optional `SerializationKnobs`; `json_record_knobs` is a live instance. +- `std.serialize` `serialize_record_doc` is the recursive record-spelling fold; `gunbc.runner_deploy_emit` is its live manifest/JSON consumer. +- `v2.lens.languages_consumer_census` baselines: `languages_consumer_census_data_decl_baseline`, `languages_consumer_census_per_language_row_baseline`, `languages_consumer_census_format_row_baseline`. ## 6. Open / boundaries -- C1 code lands in still-wolf-292 / PR #6045 — this capture PR is docs + roadmap authority only. +- The remaining work is emitter migration, not another model declaration. - Regime-1 grammar-inverse language emit stays out of scope (v2 `TargetModel` rows). -- `import_grouping` on deleted `FormatModel` — language-emit-only if it survives at all; do not carry into `SerializationKnobs`. +- Language-emission `import_grouping` stays outside `SerializationKnobs`. ## Dissolution trigger (DESIGN §6) -Delete this doc when all three knob models are collapsed into one: FormatModel deleted, OutputFormat dissolved into ConfigFormat + CommentSyntax + LayoutProtocol + SerializationKnobs, and every record-emitting format routes through serialize_record — byte-identical-witnessed on runner manifest, gitignore, and the manifest-text vs JSON swap test. +Delete this doc when the C5 digest/accelerator tail is classified by semantic grain and every true record projection routes through `std.serialize` `serialize_record_doc` with byte-identical witnesses; presentation-only lists explicitly remain on `std.render`. The legacy FormatModel/OutputFormat collapse, runner manifest/JSON swap, gitignore line-layout de-fork, dnsmasq boundary, and CSS typed-row migration are already complete. diff --git a/docs/plans/language-target-self-host-frontier.md b/docs/plans/language-target-self-host-frontier.md index bcb1ecb5ae3..159c83c6770 100644 --- a/docs/plans/language-target-self-host-frontier.md +++ b/docs/plans/language-target-self-host-frontier.md @@ -29,17 +29,16 @@ The whole point of exotic-first is that the curly-brace family *confirms* the de | --- | --- | --- | | **F0** | `emit` / `emit_module` pipeline (walks TargetModel edges backward; new target = rows, no pipeline edit) | ✓ done | | **F1** | `TargetModel` 4-edge + grammar-inverse translation rows | ✓ done | -| **F2** | VEP (`TargetValueExpressionProjection`) — the general body producer | **partial** (rust: `^rust_token_unwired_{else,loop,match,fat_arrow}`, `rust.dag:1148-1176`) · partial (TS: match/loop/bind-in unwired) · **absent** (python, ecmascript) | +| **F2** | VEP (`TargetValueExpressionProjection`) — the general body producer | **partial** (rust: `^rust_token_unwired_{else,loop,match,fat_arrow}`, `v2.extdeps.languages.rust` `rust_value_expression_projection`) · partial (TS: match/loop/bind-in unwired) · **absent** (python, ecmascript) | | **F3** | `BlockEvaluationMode` statement spine (`ValueProducing` vs `StatementSequenced`) | ✓ type exists; TS's `StatementSequenced` arm produces the correct fail-closed refusals | -| **F4** | `ProcessProgram` transport + `run_emit_host`; executable identity **bound per extdeps transport row** (`HostTransportDescriptor` / `ProcessProgram`, `host_transport.dag`), compiler dispatch **generic** | ✓ machinery; **DEFECT: dispatch is a central switch** — `host_tool_program_name` (`emit_host.dag:164-172`) is `if cargo … else if cc … else reject`, so every new tool edits one function (contradicts F0). Fix = row-bound exe identity + generic dispatch, **not** another switch branch | -| **F5** | self-host frontier runner (`run_test_claim_module_emit_vs_eval`: emit → build → run → compare-to-eval) | ✓ machinery **for Rust only**, run **OFFLINE** (excluded from discovery). Rust is **not** self-hosted: `compiler_frontier_self_emitted_baseline = 0` of `compiler_frontier_module_count_expected = 27` (`src/v2/compiler/self_host/frontier.dag`) | +| **F4** | `ProcessProgram` transport + `run_emit_host`; executable identity **bound per extdeps transport row** (`v2.std.host_transport` `HostTransportDescriptor` / `ProcessProgram`), compiler dispatch **generic** (`v2.compiler.emit_host` `process_program_name`) | ✓ done — `HostToolProgram.executable` is carried by the row and generic dispatch returns that value; target-specific work is only to configure a runtime row where one is absent | +| **F5** | self-host frontier runner (`v2.compiler.emit_host` `run_test_claim_module_emit_vs_eval`: emit → build → run → compare-to-eval) | ✓ machinery **for Rust only**, run **OFFLINE** (excluded from discovery). Rust is **not** self-hosted: `v2.compiler.self_host.frontier` `compiler_frontier_emitter_produced_count` is pinned to `v2.compiler.self_host.emitter_producer_provenance` `emitter_produced_baseline = 0`; `v2.compiler.self_host.frontier` `compiler_frontier_roster_count` derives the roster size. | | **F6** | `solve` — **structural** = existing `solve_constraints` / `ConstraintGraph` authority (extend, no fork); **numerical** = *absent* typed gap (finite measure + `TerminationProof`, typed residual-acceptance contract, extdeps solver handler) | **off critical path** — not needed for emit-to-simulator; see solve doc | -| **F7** | declaration emission generic over target (`emit_semantic_decl.dag`) | **FORKED — `emit_semantic_decl.dag` is rust-hardwired**; de-fork to row-driven per-target decl spellings is a front-loaded barrier, sibling to the F4 de-fork | +| **F7** | declaration emission generic over target (`v2.compiler.emit_semantic_decl` `emit_semantic_type_decl`) | ✓ done — the declaration emitter accepts a `TargetModel` and reads its emission bundle through `v2.std.compilers.semantic_decl_emission` `semantic_decl_emission_from_target` | -### The two highest-leverage shared dependencies (do these once, everyone inherits) +### The highest-leverage shared dependencies (do these once, everyone inherits) -1. **F4 exe-identity de-fork** — today executable identity is chosen by a central `host_tool_program_name` switch (`emit_host.dag:164-172`: `if cargo … else if cc … else reject`), which gates **bar-c for every language** and forces a branch edit per tool (contradicts F0's "new target = rows, no pipeline edit"). Bind exe identity in each extdeps transport row (`HostTransportDescriptor` / `ProcessProgram`, `host_transport.dag`) and make compiler dispatch **generic**; then each target's *already-declared* runtime row runs through the typed self-host path with no pipeline edit. Highest-leverage de-fork on the board. **F7 (decl-emission de-fork of the rust-hardwired `emit_semantic_decl.dag`) is its sibling barrier.** -2. **F2 VEP completion** — wire the unwired forms **once** (rust's `^rust_token_unwired_{else,loop,match,fat_arrow}`; TS's match / loop / bind-in) in the `StatementSequenced` arm; the family inherits body breadth. Python additionally needs its *first* VEP edge. +1. **F2 VEP completion** — wire the unwired forms **once** (rust's `^rust_token_unwired_{else,loop,match,fat_arrow}`; TS's match / loop / bind-in) in the `StatementSequenced` arm; the family inherits body breadth. Python additionally needs its *first* VEP edge. --- @@ -47,27 +46,27 @@ The whole point of exotic-first is that the curly-brace family *confirms* the de | target | family | current bar (verified) | honest end-state | key deps | stress axis | | --- | --- | --- | --- | --- | --- | -| **rust** | compiled | compiled; bar-c; F2 **partial** (`^rust_token_unwired_{else,loop,match,fat_arrow}`, `rust.dag:1148-1176`); F5 emit-vs-eval fixture **OFFLINE** | **`SeedRetained` — 0/27 self-emitted** (`compiler_frontier_self_emitted_baseline = 0`, `frontier.dag`); reference model, **NOT self-hosted** | F2 completion; F5 self-host generalization | (reference model) | -| **cpp — Phase-0-C** | compiled | bar-c via `cc`, proven by an **OFFLINE** witness in `test/claim/execution/` (excluded from discovery) | bar-c green (offline); self-host N/A at this phase | F4(`cc`) row-bound, F5-generalize | (confirms) | +| **rust** | compiled | compiled; bar-c; F2 **partial** (`^rust_token_unwired_{else,loop,match,fat_arrow}`, `v2.extdeps.languages.rust` `rust_value_expression_projection`); F5 emit-vs-eval fixture **OFFLINE** | **`SeedRetained` roster; zero producer-qualified emissions** — `v2.compiler.self_host.frontier` `compiler_frontier_emitter_produced_count` equals `v2.compiler.self_host.emitter_producer_provenance` `emitter_produced_baseline = 0`, and `seed_emitter_behavioral_green_count` equals `seed_emitter_behavioral_green_baseline = 0`; reference model, **NOT self-hosted** | F2 completion; F5 self-host generalization | (reference model) | +| **cpp — Phase-0-C** | compiled | bar-c via `cc`, proven by an **OFFLINE** witness in `test/claim/execution/` (excluded from discovery) | bar-c green (offline); self-host N/A at this phase | F5-generalize | (confirms) | | **cpp — full C target** | compiled | **below bar-a** for full C | blocked — needs **monomorphization** (grep-**zero** in tree), **closure conversion**, a **discriminant-tag row kind**, **multi-file (header/impl) projection**, and **ABI/linkage** — none present | monomorphization, closure conversion, tag-row kind, multi-file projection, ABI/linkage | (confirms — hard) | -| **go** | compiled | **skeleton** — needs TargetModel buildout | **self-host** (first non-rust self-host — the F5 generalization proof), once built | TargetModel buildout, F4(`go`) row-bound, surface spellings, F5 | **self-host axis** | -| **java / kotlin / swift** | compiled | **skeleton** — need TargetModel buildout | bar-c → self-host | TargetModel buildout, F4(tool) row-bound, spellings, inherit F2/F3/F5 | (confirms — parallel) | -| **typescript** | interpreted | F2 **partial** (match/loop/bind-in unwired); **bar-c RED** — runtime row present but `node`/`npx` unregistered | self-host | F4(`node`/`npx`) row-bound, F2 completion (match/loop/bind-in), operator catalog | self-host axis | -| **python** | interpreted | **no VEP edge — add-only** | bar-c → self-host | F2 *first* edge, operator catalog, F4(`python3`) row-bound | self-host axis | +| **go** | compiled | **skeleton** — needs TargetModel buildout | **self-host** (first non-rust self-host — the F5 generalization proof), once built | TargetModel buildout, surface spellings, F5 | **self-host axis** | +| **java / kotlin / swift** | compiled | **skeleton** — need TargetModel buildout | bar-c → self-host | TargetModel buildout, runtime-row configuration, spellings, inherit F2/F3/F5 | (confirms — parallel) | +| **typescript** | interpreted | F2 **partial** (match/loop/bind-in unwired); runtime row is configured (`v2.extdeps.languages.typescript` `ts_runtime_row`), but this pre-un-shelve map does not establish current bar-c execution | self-host | F2 completion (match/loop/bind-in), operator catalog | self-host axis | +| **python** | interpreted | **no VEP edge — add-only** | bar-c → self-host | F2 *first* edge, operator catalog | self-host axis | | **ecmascript** | interpreted | **orphan (0 consumers)** | **decide first**: adopt as TS's JS base, or delete | (adoption decision) | — | | **lean** | expression/ML | **below bar-a** — type model + anchor test only, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs) | self-host on an *expression* spine (not statement), once a TargetModel is built | committed TargetModel, F3 generalization (expression-mode), F2, F5 | self-host axis (spine falsifier) | -| **verilog** | HDL | **below bar-a** — type model + anchor, **no committed TargetModel**; **11** `body_lexeme:String` fields to decompose | **bar-c green + frontier row `self-host: N/A (hardware)`** | committed TargetModel, decompose `body_lexeme` → structured, F4(`verilator`/`iverilog`) row-bound | **emit-generality (concurrent)** | -| **spice** | analog format | **bar-b only** — the witness compares emitted text to a **golden** (`spice_rc_ngspice_oracle_test.dag:18-25`); it **never runs ngspice** | bar-c green + frontier row `self-host: N/A (analog)`. **No Modelica carrier in-tree** — dual-emit is future, not present | F4(`ngspice`) row-bound (bar-b → bar-c); Modelica carrier does not yet exist | **emit-generality (continuous)** | -| **llvm_ir** | IR/backend | **below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs) | bar-c green + frontier row `self-host: N/A (no runtime)` — the Rust/cargo-free lowering path, once a TargetModel is built | committed TargetModel, F4(`llc`/`clang`) row-bound | **emit-generality (SSA)** | -| **wasm** | IR/backend | has a **TargetModel** (bundle/lex/binding_spellings) BUT **bar-c unreachable** — `runtime_row: target_emit_host_runtime_row_unconfigured` (HostRuntimeRowAbsent, `wasm.dag:624-632`) | bar-c green + frontier row `self-host: N/A` — **blocked on configuring the runtime row** | configure runtime row, F4(`wasmtime`) row-bound | emit-generality (stack machine) | -| **machine_code / ptx** | ISA/GPU | **below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs) | bar-c green + frontier row `self-host: N/A`, once a TargetModel is built | committed TargetModel, F4(assembler/`ptxas`) row-bound | emit-generality (ISA) | +| **verilog** | HDL | **below bar-a** — type model + anchor, **no committed TargetModel**; **11** `body_lexeme:String` fields to decompose | **bar-c green + frontier row `self-host: N/A (hardware)`** | committed TargetModel, decompose `body_lexeme` → structured, configure the `verilator`/`iverilog` runtime row | **emit-generality (concurrent)** | +| **spice** | analog format | **bar-b only** — the witness compares emitted text to a **golden** (`v2.test.formats.spice_rc_ngspice_oracle` `spice_rc_ngspice_op_holds`); it **never runs ngspice** | bar-c green + frontier row `self-host: N/A (analog)`. **No Modelica carrier in-tree** — dual-emit is future, not present | configure the `ngspice` runtime row (bar-b → bar-c); Modelica carrier does not yet exist | **emit-generality (continuous)** | +| **llvm_ir** | IR/backend | **below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs) | bar-c green + frontier row `self-host: N/A (no runtime)` — the Rust/cargo-free lowering path, once a TargetModel is built | committed TargetModel, configure the `llc`/`clang` runtime row | **emit-generality (SSA)** | +| **wasm** | IR/backend | has a **TargetModel** (bundle/lex/binding_spellings) BUT **bar-c unreachable** — `runtime_row: target_emit_host_runtime_row_unconfigured` (`v2.extdeps.languages.wasm` `wasm_target_model`) | bar-c green + frontier row `self-host: N/A` — **blocked on configuring the runtime row** | configure the `wasmtime` runtime row | emit-generality (stack machine) | +| **machine_code / ptx** | ISA/GPU | **below bar-a** — type model + anchor, **no committed TargetModel** (0 `target_model` / `translation_rules_node` refs) | bar-c green + frontier row `self-host: N/A`, once a TargetModel is built | committed TargetModel, configure the assembler/`ptxas` runtime row | emit-generality (ISA) | --- ## Sequencing — Rust-as-model, then stress (dependency-ordered) - **Phase A — now-ish (pre-un-shelve):** this map + the `solve` rationale. No emit code. ← *we are here* -- **Phase B — foundation de-fork (the barrier; everything downstream inherits):** F4 exe-identity de-fork (row-bound identity + generic dispatch) + F7 decl-emission de-fork (`emit_semantic_decl.dag`) + F2 VEP completion (rust + TS). Once B lands, C/D/E run largely in parallel. +- **Phase B — foundation completion (the barrier; everything downstream inherits):** F2 VEP completion (rust + TS). Once B lands, C/D/E run largely in parallel. - **Phase C — self-host axis proof:** generalize F5 past Rust to **Go** (first non-Rust self-host) — and land Rust's own self-host (0/27 today). This is the real "does the seed-shrink story generalize" milestone. If it holds, java/kotlin/swift are near-mechanical parallel fan-out. - **Phase D — emit-generality axis (parallel):** Verilog · SPICE · LLVM-IR to bar-c + frontier rows. Verilog and LLVM-IR first need a **committed TargetModel** (both below bar-a today); SPICE needs its witness to actually run ngspice (bar-b → bar-c). Each decomposes its `body_lexeme:String` scars and binds its simulator/toolchain transport in a row. This is where the design gets *stressed*; a construct that won't lower produces a typed, located refusal that *names the design gap* — the refusal is the product. - **Phase E — interpreted self-host:** TS → Python (Python inherits TS's VEP completion). @@ -79,7 +78,7 @@ Each language is **priced by the design risk it displaces**, not by completeness ## Staffing note (for continuous dispatch) -Off this map, the natural fan-out is **one child session per language axis**, gated on Phase B. The dependency structure that makes this safe: **B is the only hard barrier** (F4 + F7 de-forks + F2 completion); after it, the self-host axis (C, then the compiled fan-out) and the emit-generality axis (D) have no cross-dependency, so they staff independently. Lean (F) and the interpreted family (E) each ride one Phase-B deliverable (F3-expression-mode and F2-completion respectively) plus their own missing TargetModel where noted. ecmascript's adopt-or-delete decision is a prerequisite gate on the interpreted family, not parallel work. +Off this map, the natural fan-out is **one child session per language axis**, gated on Phase B. The dependency structure that makes this safe: **B is the only hard barrier** (F2 completion); after it, the self-host axis (C, then the compiled fan-out) and the emit-generality axis (D) have no cross-dependency, so they staff independently. Lean (F) and the interpreted family (E) each ride one Phase-B deliverable (F3-expression-mode and F2-completion respectively) plus their own missing TargetModel where noted. ecmascript's adopt-or-delete decision is a prerequisite gate on the interpreted family, not parallel work. ## Dissolution trigger (DESIGN §6) diff --git a/docs/plans/typescript-gap-census.md b/docs/plans/typescript-gap-census.md index 47e42c84257..e9d446109bf 100644 --- a/docs/plans/typescript-gap-census.md +++ b/docs/plans/typescript-gap-census.md @@ -28,8 +28,8 @@ 6. **#6 enum / disj union** — VEP. Witness: `ts_enum_union_emit_by_execution_exact_holds` (`typescript_enum_union_emit_by_execution_test.dag`). 7. **#7 module import** — VEP. Witness: `ts_import_emit_by_execution_exact_holds` (`typescript_import_emit_by_execution_test.dag`). 8. **#8 effect apply** — VEP. Witness: `ts_effect_io_emit_holds` (`typescript_effect_io_emit_test.dag`). -9. **#9 fold_call body via translate** — VEP. Witness: `fold_call_closure_emit_keystone_holds` (`fold_call_closure_emit_test.dag`). -10. **#10 operators (arith/cmp)** — VEP with **ad-hoc test catalog only** (`add_body_ts_emit_catalog_minus_discriminates`, `add_body_ts_emit_missing_catalog_rejects`). Default `ts_operator_realizations_catalog_node()` enrolls **OpAdd only** (`typescript.dag:640`) — see #16. +9. **#9 fold_call body via translate** — VEP. Witness: `v2.test.manual.fold_call_closure_emit` `fold_call_emit_holds`; the paired `fold_call_swap_discriminates` is the red control. +10. **#10 operators (arith/cmp)** — VEP with **ad-hoc test catalog only** (`add_body_ts_emit_catalog_minus_discriminates`, `add_body_ts_emit_missing_catalog_rejects`). Default `v2.extdeps.languages.typescript` `ts_operator_realizations_catalog_node` enrolls **OpAdd only** — see #16. ### FAIL-CLOSED (emit explicitly Rejected — named) @@ -38,11 +38,11 @@ ### FAIL-OPEN (compiler-scale; no green bar (b)+(c) on default model today) -1. **#13 match / coproduct dispatch** — `match_form.match_token = ^ts_token_unwired_match` (`typescript.dag:623`); no TS match witness; compiler uses `Match` heavily (`05_eval.dag`). -2. **#14 bind-in scoping** — `let_form.in_token = ^ts_token_unwired_bind_in` (`typescript.dag:606`). -3. **#15 loop form wiring** — `loop_form.loop_token = ^ts_token_unwired_loop` (`typescript.dag:609`). -4. **#16 default operator catalog** — `ts_operator_realizations_catalog_node()` rows = `[ts_add_operator_realization_row()]` only (`typescript.dag:640–641`). Algebra ops miss on default model (`add_body_ts_emit_missing_catalog_rejects`). -5. **#17 grammar-inverse rows beyond add** — committed `ts_translation_rules_node()` has **1** child (`fn_add`); witness bundle `ts_translation_rules_witness()` expects **3** (add + type_alias + pr3) (`typescript.dag:1381–1414`). +1. **#13 match / coproduct dispatch** — `match_form.match_token = ^ts_token_unwired_match` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`); no TS match witness; compiler uses `Match` heavily (`05_eval.dag`). +2. **#14 bind-in scoping** — `let_form.in_token = ^ts_token_unwired_bind_in` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`). +3. **#15 loop form wiring** — `loop_form.loop_token = ^ts_token_unwired_loop` (`v2.extdeps.languages.typescript` `ts_value_expression_projection_full`). +4. **#16 default operator catalog** — `v2.extdeps.languages.typescript` `ts_operator_realizations_catalog_node` rows = `[ts_add_operator_realization_row()]` only. Algebra ops miss on default model (`add_body_ts_emit_missing_catalog_rejects`). +5. **#17 grammar-inverse rows beyond add** — committed `v2.extdeps.languages.typescript` `ts_translation_rules_node` has **1** child (`fn_add`); `ts_translation_rules_witness` carries **2** rows (add + type_alias), while `ts_pr3_translation_rules_witness` carries **3** (add + type_alias + pr3). Type_alias and pr3 are witnessed candidates but neither is enrolled in the committed bundle. 6. **#18 branch dispatch** — compiler uses `Branch` (`04_infer` / `05_eval`); zero TS emit witnesses. 7. **#19 tsc-green / emit_host oracle** — §5 spec-without-execution crack. Sole consumer path: `ts_host_transport_descriptor` + `emit_host_gate.dag`. **`typescript_descriptor_node_ts_node_run_add_holds` FAIL** (wet `claim_batch`); **`emit_host_gate_passes` FAIL** (wet). Bar (c) red even for add. 8. **#20 whole `src/v2` → TS** — no module; Route-A tsc analogue not started (terminal slice E). @@ -63,7 +63,7 @@ 1. **A. Land this census** (this plan) — audit-first record, generated md. 2. **A2. tsc-green oracle REAL on existing VEP-green slices (#19 pulled forward)** — per-construct `tsc` acceptance on #1–#9 before stacking breadth. Converts string-green families into compile-green. Highest-value foundation work. -3. **B. Cheap row extensions (#17)** — enroll type_alias + pr3 rows into committed `ts_translation_rules_node`; rows only, no new TargetModel surface. +3. **B. Cheap row extensions (#17)** — enroll the type_alias row from `v2.extdeps.languages.typescript` `ts_translation_rules_witness` and the pr3 row from `ts_pr3_translation_rules_witness` into committed `ts_translation_rules_node`; rows only, no new TargetModel surface. 4. **C. Operator catalog (#16)** — proceed **only** if genuinely row-derivation onto the default model; if it needs a new TargetModel surface → load-bearing → sign first. 5. **D. HOLD for parent sign:** Match (#13) + loop/bind (#14–#15) + Branch (#18) — compiler-scale TargetModel surfaces. 6. **E. Whole-tree Route-A tsc (#20)** — terminal.