diff --git a/.githooks/pre-push b/.githooks/pre-push index 8f3d3dc9169..20fcfd0add3 100755 --- a/.githooks/pre-push +++ b/.githooks/pre-push @@ -83,6 +83,7 @@ fresh_artifact_path() { docs/plans/ci-floor-fractal-gantt.md*) return 0 ;; docs/plans/representation-minimization.md*) return 0 ;; docs/plans/reference-grounding-migration.md*) return 0 ;; + docs/plans/typescript-gap-census.md*) return 0 ;; dsl/**) return 0 ;; src/v2/**) return 0 ;; esac diff --git a/docs/plans/typescript-gap-census.md b/docs/plans/typescript-gap-census.md new file mode 100644 index 00000000000..8dde5a08093 --- /dev/null +++ b/docs/plans/typescript-gap-census.md @@ -0,0 +1,75 @@ +# TypeScript first-class gap census — discriminating construct audit (Lane C / Track T) + +**Status:** audit-first discriminating census · **approved 2026-07-01** (loyal-bee-794) · linked from `ROADMAP.md` `5-ts-first-class` · companion to `v2-self-hosting.md` Track T. **`dsl/gunbc/plans/typescript_gap_census.dag` is the authority** (DESIGN §6); `docs/plans/typescript-gap-census.md` is its generated projection (PlanArtifact). + +**Method:** enumerate construct families `src/v2` actually uses (compiler substrate behaviors in `src/v2/compiler/*` + TargetModel emit surfaces in `src/v2/extdeps/languages/typescript.dag`). For each family report three independent bars: (a) grammar-inverse row enrolled on the committed TargetModel node, (b) VEP / pipeline emits the expected **TypeScript source string** (witness PASS), (c) **`tsc` / emit_host accepts the output** (consumer green-by-execution). Every FAIL names a witness or authority site — not a stub count. + +> **Two-bar clarification (parent reframe 2026-07-01).** The GREEN column below is **bar (b) only** — VEP produces the expected TS source string. Bar (c) — `tsc` actually compiles the emitted output — is **UNMET even for `add`**: `typescript_descriptor_node_ts_node_run_add_holds` (`src/v2/test/claim/manual/typescript_descriptor_node_run_test.dag`) and `emit_host_gate_passes` (`dsl/tools/emit_host_gate.dag`) both **FAIL wet** in execution. A construct is not genuinely first-class until bar (c) is green. **Do not stack breadth on a red tsc foundation.** + +--- + +## 1. Baseline (merged on main, not stub PRs) + +- #5695 — Char atom-realization + green typed-fn emit +- #5701 — FieldAccess + RecordConstruct + `tsc --noEmit` oracle (source-string witnesses; bar (c) still red — see #19) +- #5704 — operators by inhabitance (test-catalog only, not default TargetModel) +- #5938 — collection-method grammar rows +- ~55 `typescript_*` / `ts_*` test fns under `src/v2/test/claim/` (manual + execution trees) + +## 2. Census table + +### VEP source-string GREEN (bar (b) witness PASS) + +1. **#1 fn add** — grammar-inverse row + full infer→emit pipeline. Witness: `add_body_ts_emit_add_fn_accepts_holds`, `typescript_add_emit_add_fn_accepts_holds` (`add_body_emit_typescript_test.dag`, `typescript_add_emit_translate_test.dag`). +2. **#2 field access** — VEP. Witness: `ts_field_access_emit_source_holds` → `"o.x"` (`typescript_field_access_emit_test.dag`). +3. **#3 record construct** — VEP. Witness: `ts_record_construct_emit_source_holds` (`typescript_record_construct_emit_test.dag`). +4. **#4 bind let IIFE** — VEP. Witness: `ts_bind_let_iife_emit_exact_holds` (`typescript_bind_let_iife_emit_test.dag`). +5. **#5 closure (value-producing)** — VEP. Witness: `ts_closure_emit_by_execution_exact_holds` (`typescript_closure_emit_by_execution_test.dag`). +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. + +### FAIL-CLOSED (emit explicitly Rejected — named) + +1. **#11 loop in statement-sequenced block mode** — `ts_loop_statement_sequenced_fails_closed_holds` (`typescript_bind_let_iife_emit_test.dag`; also `typescript_closure_emit_by_execution_test.dag`). `.dag` loop emits; TS `StatementSequenced` mode rejects. +2. **#12 closure in statement-sequenced block mode** — `ts_closure_statement_sequenced_fails_closed_holds` (same files). + +### 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_mvp1_translation_rules_node()` has **1** child (`fn_add`); witness bundle `ts_mvp1_translation_rules_witness()` expects **3** (add + type_alias + pr3) (`typescript.dag:1381–1414`). +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_mvp1_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). + +## 3. Discriminating counts + +- **VEP source-string GREEN families:** 9 (#1–#9; #10 green only with ad-hoc catalog) +- **FAIL-CLOSED:** 2 (#11–#12) +- **FAIL-OPEN compiler-scale gaps:** 8 (#13–#20) +- **tsc-green (bar c):** 0/N wet — add fixture attempted, red in execution (#19) +- **Grammar-inverse rows:** 1 committed / 3 in witness bundle / ~15 wave2a productions defined + +## 4. Size call + +**LARGE multi-slice** — not a single row PR. Cheap tranche = grammar-row extensions (#17) + operator catalog derivation onto default TargetModel if row-only (#16). Load-bearing tranche = Match (#13) + loop/bind forms (#14–#15) + Branch (#18) — **HOLD for parent sign** before authoring TargetModel surfaces. Whole-tree tsc (#20) is terminal after per-construct gaps close. + +## 5. Sequencing (revised 2026-07-01) + +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_mvp1_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. + +**Priority note:** Lane C is language-breadth; operator retains burn-down sequencing call. Proceed A → A2 → B meanwhile; HOLD D for both parent sign and operator priority. + +## Dissolution trigger (DESIGN §6) + +Delete this census once every FAIL-OPEN row (#13–#20) is closed with execution-grounded witnesses and bar (c) tsc-green holds on the default TargetModel — the audit record is superseded by the substrate facts it enumerated. diff --git a/docs/plans/v2-self-hosting.md b/docs/plans/v2-self-hosting.md index d4bf9049af7..ad4a5c86f33 100644 --- a/docs/plans/v2-self-hosting.md +++ b/docs/plans/v2-self-hosting.md @@ -16,13 +16,13 @@ The state-of-play below was verified 2026-06-21. What moved in the two days sinc - **IMPROVED — the gap now has an owner and a construction-first fix.** The reconciliation endgame is **bright-stag-owned**: a model-first *single-authority* kill — **derive** the hand-maintained copy-lists FROM the emitted-module authority so the emitted↔hand drift becomes **unwritable** (the `invert-hand-maintained` move), with crisp-carp's `regen-verify` floor gate as the weaker post-hoc backstop layered on top. roadmap **`5-regen-verify` pulled forward**. cool-carp owns the *immediate* reconcile (fix the copy-lists + re-seed the 4 + verify clean) ahead of the construction fix. - **IMPROVED — sequencing crystallized (emitter-first).** Order is now fixed: emitter-correctness settles (jolly-cat's Route-A lane; the corpus-emit surface measured at **~12,600 `E0308`**) → **single regen cutover** (bright-stag reconciliation) → `regen-verify` green → §7 fixpoint provable. Cutting over mid-emitter-churn re-drifts immediately, so the cutover is the *closing* step, not concurrent. This refines *Forced precondition order* step 3 below (it now has an owner + an ordering). - **DECIDED — open question #1 (reopen direction).** Resolved to **(a)**: finish the Route-A green bootstrap (continue `emitter/seed-green-integration`, do **not** restart into a pure-`.dag` coherence reset). Anchored; do not re-litigate. -- **UNTOUCHED (still the wall, unchanged since 2026-06-21):** the Route-A last mile — the emitted crate still does **not** `cargo build` green (the `dsl_compile_clean` gate still only proves *well-typed*, not *built*). Track B / Stage C is still fail-closed (no real-digest match; comparison substrate still operator-pending, merry-crab-687). Track T (TypeScript) is still proven only on the `add` slice. The 590s+ whole-tree resolve is still the practical wall. None of these moved. +- **LANDED — Route-A last mile (2026-06-25..28, #5777/#5873; re-verified cool-ant-875 2026-07-01).** `regen_stage0 --emit-fresh` → faithful assembled crate → `cargo build` debug+release is **0 errors** (`route_a_emit_fresh_cargo_green_test` witness). `dsl_compile_clean` still only proves well-typed emit (not built); the execution witness is the receipt. **Still open:** Track B / Stage C (no real-digest match; comparison substrate operator-pending, merry-crab-687). Track T (TypeScript) proven only on the `add` slice. The 590s+ whole-tree resolve is still the practical wall. - **Tracked elsewhere (not a self-host milestone):** the CI-fleet resource problem (session over-allocation, CI-floor under-sharding, resolve-cache) → `compute-envelope-model.md`; the std fork census → `dsl-v2-defork-audit.md`. The session-spawn cap *was* fixed operationally 2026-06-23 (per-session RAM reservation 31g→4g, ~30 sessions/host) — an infra fix, orthogonal to this track. ## 0. State of play (what's done, what's open) - **Front-end — DONE, proven at scale.** `src/v2/` is 100% `.dag` (698 modules, 0 `.rs`; all Rust is the `src/v1` seed, ~154k lines). Full pipeline present: `01_tokenize → 02_parse → 03_resolve/name_resolve/ingest → 04_infer → 05_emit/eval → 06_translate → 07_target_carriers`. The historical blockers are fixed and merged: parse-perf (#5093 ParseTable memo, #3661), resolve/infer cost (#5258 the O(2^depth) double-resolve fix, #5266, #5146), cross-file names (#5271 Route C Phase B, #5154 filepath→QualifiedName). gap-4 (let-stmt in match arm) merged #5369; whole-tree parse-regression scanner added #5406. *Nuance:* per-file parse is fast, but a **combined `dsl`+`src/v2` whole-tree resolve is still heavy (590s+)** — "no perf wall" means the fixed blockers, not an instant full-tree resolve. -- **Emit / Route A — runs whole-tree, but the emitted crate doesn't build yet.** `gunbc compile --source-root … --target rust` exists and the CI `dsl_compile_clean` gate runs it over `[src/v2, dsl]`, gating all of batch-2. **But the gate only proves the tree is well-typed** (emit runs to completion, writes `$OUT`, then `rm -rf $OUT`). It does **not** `cargo build` the emitted whole-tree crate. Only the emit-host MVP smokes compile tiny fixtures. **The green build of the emitted crate is the open Route-A last mile.** +- **Emit / Route A — whole-tree emit + faithful `--emit-fresh` crate builds green (#5777/#5873).** `gunbc compile --source-root … --target rust` exists and the CI `dsl_compile_clean` gate runs it over `[src/v2, dsl]`, gating batch-2 (well-typed emit only — writes `$OUT`, then `rm -rf $OUT`). The **cargo-green** receipt is `regen_stage0 --emit-fresh ` → `cargo build` (debug+release), proven by `route_a_emit_fresh_cargo_green_test`. - **Fixed-point proof — fail-closed (not achieved).** `self_host.dag`'s `self_host_fixed_point_validate` **unconditionally returns `Rejected`** (`self_host_runner_not_realized`) — the honest contract until Stage C. `self_host_fixed_point_digests_match` (`==` over `content_hash`) is realized but de-risked only on fixture stages. The whole-compiler fixed point over real digests does not yet run. - **Emitter — genuinely multi-target.** One `fold_node` catamorphism in `06_translate.dag`; emit selects a target's `target_model_edge_translation_rules` and walks the same rows **backward** (`grammar_relation_row_reverse_parse_selection`). 14 targets in `src/v2/extdeps/languages/` (rust, python, go, bash, dag, cpp, typescript, kotlin, swift, java, lean, ptx, verilog, …), 5 in `dsl`. A new target is **data rows, never a new emitter**. @@ -33,11 +33,11 @@ The state-of-play below was verified 2026-06-21. What moved in the two days sinc Get the v2-emitted Rust compiler to build and reproduce itself. 1. Emit whole tree `--target rust` — **done** (well-typed under CI gate). -2. `cargo build` the emitted crate green — **open** (the last mile). +2. `cargo build` the emitted crate green — **done** (#5777/#5873; `regen_stage0 --emit-fresh` witness). 3. `regen_stage0` from the emitted crate; replace the hand-Rust seed. 4. Flip the lockstep / fixed-point gate from fail-closed to asserting the real `content_hash` digest match (Stage C). -Unmerged work: branch `emitter/seed-green-integration @ 239ff284d5` (**not in main**) carries 6 commits toward a green regen — import-completeness (E0425), List→host-`Vec`, Int-as-generic-arg→`i64`, `regen_stage0` patch, + 2 integration commits. PR **#5325 is CLOSED, not merged.** Recent emitter slices on main: #5413 (length→count, phantom-marker derives, Measure-alias E0560 peel, E0308 Box-deref cluster); MachineWidth is **#5397** (E0107), a separate PR. +**Route-A cargo-green landed on main** (#5777 emitter fixes → 0 rustc errors; #5873 two-generation regen cutover + `regen --verify` CI gate). Branch `emitter/seed-green-integration` content is absorbed — the branch is stale vs `main` and can be retired. PR **#5325** remains closed (superseded by #5873). ### Purity: no stage0 hand-edits (the requirement, and the enforcement gap) @@ -46,10 +46,10 @@ Unmerged work: branch `emitter/seed-green-integration @ 239ff284d5` (**not in ma The requirement — **v2 emits its own seed; no human stage0 patches** — is *modeled, currently unmet, and un-enforced.* `src/v2/workflow/bootstrap.dag` is the authority and states it exactly ("seed→stage0→stage1→stage2, fixpt stage1==stage2 … seed used once; v2 is never in the loop again", DESIGN §7), including the trust machinery to retire the seed (`SeedHonestyDischarge`, `DiverseCompilationAgreement`/`IndependentCompilerPair` = Diverse Double-Compiling, the Thompson trusting-trust defense). But: - **The seed is hand-maintained today.** `regen_stage0.rs` carries `HAND_MAINTAINED_STAGE0_FILES` + `patch_*` (e.g. `patch_bootstrap_dag_collect`) that compensate for emitter gaps — each a "stage0 hand-edit standing in for a thing v2 should emit itself," honestly marked with a dissolve-on pointing at the emitter fix. (Gotcha: regen has pre-existing codegen drift, so focused PRs hand-edit the `.rs` seed mirror rather than commit a full regen — itself a symptom of the gap.) -- **The no-drift gate is real but not wired.** `regen_stage0 --verify` (`verify_stage0_matches` — "committed stage0 matches fresh self-compile") exists, but a grep of the CI floor (`src/v2/workflow`, `dsl/tools`, `dsl/gunbc`, `dsl/test`) finds it nowhere. The `Stage0LockstepGate` that would wire it in is the content of **closed/unmerged #5325**. So hand-drift goes silently uncaught — erosion by one more honest-looking `patch_*` at a time. +- **The no-drift gate is wired (#5873).** `regen_stage0 --verify` runs in the CI floor via `RegenVerifyGate` → `regen_verify_gate_passes` (`src/v2/workflow/ci_floor_plan.dag`). It enforces no drift on **generated** `GENERATED_STAGE0_FILES`; `HAND_MAINTAINED_STAGE0_FILES` are copied through by design. Closed #5325's `Stage0LockstepGate` was superseded by #5873. **Still open:** dissolve `patch_*` / hand-maintained copies so the emitter owns the whole seed (roadmap `5-dissolve-patches`). - **bootstrap.dag is 🟡 scaffold** — structural wiring only, placeholder hashes (dissolve-on T-15/T-20 `content_hash` supplying real per-stage merkle digests), so it does not yet *prove* convergence. -**This gate is the keystone for both the purity requirement and a trustworthy cutover.** It is what makes "no stage0 hand-edits" enforceable; without it the requirement can only erode. +**The regen-verify gate is the keystone for a trustworthy cutover** — it now runs in CI (#5873), but hand-maintained seed copies and `patch_*` remain until `5-dissolve-patches` lands. ### Track B — the fixed-point proof (Stage C) @@ -69,9 +69,9 @@ So "delete stage0" decomposes — `src/v1` also provides the **CLI bins** (`clai **Forced precondition order (each gates the next):** -1. Whole-tree emit → `cargo build` green (Track A last mile). +1. Whole-tree emit → `cargo build` green — **done** (#5777/#5873; `regen_stage0 --emit-fresh` witness). 2. Real fixed point: `self_host_fixed_point_digests_match` over real `content_hash` (Track B / Stage C; dissolve the placeholder hashes, T-15/T-20). -3. `regen_stage0 --verify` green **and wired into CI** (the `Stage0LockstepGate`, closed #5325) + all `patch_*` / `HAND_MAINTAINED_STAGE0_FILES` dissolved so the emitter emits the whole seed. **This is the step that actually retires "stage0 hand-edits"** and makes the cutover trustworthy. *(Owner + ordering, per #5639: the single regen **cutover** is bright-stag-owned — derive the copy-lists from the emitted-module authority so the drift is unwritable — and lands **after** the emitter largely settles (jolly-cat's emitter-correctness lane), since each emitter fix shifts what a regen produces. crisp-carp's `regen-verify` floor gate is the backstop. roadmap `5-regen-verify` pulled forward.)* +3. `regen_stage0 --verify` wired into CI — **done** (#5873 `RegenVerifyGate`) + all `patch_*` / `HAND_MAINTAINED_STAGE0_FILES` dissolved (**open**, roadmap `5-dissolve-patches`) so the emitter emits the whole seed. **This is the step that actually retires "stage0 hand-edits"** and makes the cutover trustworthy. *(Owner + ordering, per #5639: the single regen **cutover** is bright-stag-owned — derive the copy-lists from the emitted-module authority so the drift is unwritable — and lands **after** the emitter largely settles, since each emitter fix shifts what a regen produces.)* 4. Seed-honesty discharge (ideally via Diverse Double-Compiling). 5. Then collapse `src/v1` to the pinned reproducible seed and delete its compiler logic **incrementally** — verify by execution, not assumption. diff --git a/dsl/gunbc/plan_registry_batch_g.dag b/dsl/gunbc/plan_registry_batch_g.dag index 357ec2b8f25..e9925ca9901 100644 --- a/dsl/gunbc/plan_registry_batch_g.dag +++ b/dsl/gunbc/plan_registry_batch_g.dag @@ -9,6 +9,7 @@ import gunbc.plans.host_effect_orchestration { host_effect_orchestration_plan } import gunbc.plans.ci_floor_fractal_gantt { ci_floor_fractal_gantt_plan } import gunbc.plans.representation_minimization { representation_minimization_plan } import gunbc.plans.reference_grounding_migration { reference_grounding_migration_plan } +import gunbc.plans.typescript_gap_census { typescript_gap_census_plan } data batch_g_plans: List = [ ci_humming_plan, @@ -18,5 +19,6 @@ data batch_g_plans: List = [ host_effect_orchestration_plan, ci_floor_fractal_gantt_plan, representation_minimization_plan, - reference_grounding_migration_plan + reference_grounding_migration_plan, + typescript_gap_census_plan ] diff --git a/dsl/gunbc/plans/typescript_gap_census.dag b/dsl/gunbc/plans/typescript_gap_census.dag new file mode 100644 index 00000000000..cdbf08319b3 --- /dev/null +++ b/dsl/gunbc/plans/typescript_gap_census.dag @@ -0,0 +1,85 @@ +module gunbc.plans.typescript_gap_census + +import gunbc.plan { Plan, DissolutionTrigger, HasTrigger } +import std.markdown { MarkdownBlock, ThematicBreak } +import gunbc.plans.md_helpers { h2, h3, p, li, ul, ol, quote } + +fn typescript_gap_census_body() -> List { + [ + p(text: "**Status:** audit-first discriminating census · **approved 2026-07-01** (loyal-bee-794) · linked from `ROADMAP.md` `5-ts-first-class` · companion to `v2-self-hosting.md` Track T. **`dsl/gunbc/plans/typescript_gap_census.dag` is the authority** (DESIGN §6); `docs/plans/typescript-gap-census.md` is its generated projection (PlanArtifact)."), + p(text: "**Method:** enumerate construct families `src/v2` actually uses (compiler substrate behaviors in `src/v2/compiler/*` + TargetModel emit surfaces in `src/v2/extdeps/languages/typescript.dag`). For each family report three independent bars: (a) grammar-inverse row enrolled on the committed TargetModel node, (b) VEP / pipeline emits the expected **TypeScript source string** (witness PASS), (c) **`tsc` / emit_host accepts the output** (consumer green-by-execution). Every FAIL names a witness or authority site — not a stub count."), + quote(blocks: [ + p(text: "**Two-bar clarification (parent reframe 2026-07-01).** The GREEN column below is **bar (b) only** — VEP produces the expected TS source string. Bar (c) — `tsc` actually compiles the emitted output — is **UNMET even for `add`**: `typescript_descriptor_node_ts_node_run_add_holds` (`src/v2/test/claim/manual/typescript_descriptor_node_run_test.dag`) and `emit_host_gate_passes` (`dsl/tools/emit_host_gate.dag`) both **FAIL wet** in execution. A construct is not genuinely first-class until bar (c) is green. **Do not stack breadth on a red tsc foundation.**"), + ]), + ThematicBreak, + h2(text: "1. Baseline (merged on main, not stub PRs)"), + ul(items: [ + li(text: "#5695 — Char atom-realization + green typed-fn emit"), + li(text: "#5701 — FieldAccess + RecordConstruct + `tsc --noEmit` oracle (source-string witnesses; bar (c) still red — see #19)"), + li(text: "#5704 — operators by inhabitance (test-catalog only, not default TargetModel)"), + li(text: "#5938 — collection-method grammar rows"), + li(text: "~55 `typescript_*` / `ts_*` test fns under `src/v2/test/claim/` (manual + execution trees)"), + ]), + h2(text: "2. Census table"), + h3(text: "VEP source-string GREEN (bar (b) witness PASS)"), + ol(items: [ + li(text: "**#1 fn add** — grammar-inverse row + full infer→emit pipeline. Witness: `add_body_ts_emit_add_fn_accepts_holds`, `typescript_add_emit_add_fn_accepts_holds` (`add_body_emit_typescript_test.dag`, `typescript_add_emit_translate_test.dag`)."), + li(text: "**#2 field access** — VEP. Witness: `ts_field_access_emit_source_holds` → `\"o.x\"` (`typescript_field_access_emit_test.dag`)."), + li(text: "**#3 record construct** — VEP. Witness: `ts_record_construct_emit_source_holds` (`typescript_record_construct_emit_test.dag`)."), + li(text: "**#4 bind let IIFE** — VEP. Witness: `ts_bind_let_iife_emit_exact_holds` (`typescript_bind_let_iife_emit_test.dag`)."), + li(text: "**#5 closure (value-producing)** — VEP. Witness: `ts_closure_emit_by_execution_exact_holds` (`typescript_closure_emit_by_execution_test.dag`)."), + 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."), + ]), + h3(text: "FAIL-CLOSED (emit explicitly Rejected — named)"), + ol(items: [ + li(text: "**#11 loop in statement-sequenced block mode** — `ts_loop_statement_sequenced_fails_closed_holds` (`typescript_bind_let_iife_emit_test.dag`; also `typescript_closure_emit_by_execution_test.dag`). `.dag` loop emits; TS `StatementSequenced` mode rejects."), + li(text: "**#12 closure in statement-sequenced block mode** — `ts_closure_statement_sequenced_fails_closed_holds` (same files)."), + ]), + 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_mvp1_translation_rules_node()` has **1** child (`fn_add`); witness bundle `ts_mvp1_translation_rules_witness()` expects **3** (add + type_alias + pr3) (`typescript.dag:1381–1414`)."), + 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_mvp1_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)."), + ]), + h2(text: "3. Discriminating counts"), + ul(items: [ + li(text: "**VEP source-string GREEN families:** 9 (#1–#9; #10 green only with ad-hoc catalog)"), + li(text: "**FAIL-CLOSED:** 2 (#11–#12)"), + li(text: "**FAIL-OPEN compiler-scale gaps:** 8 (#13–#20)"), + li(text: "**tsc-green (bar c):** 0/N wet — add fixture attempted, red in execution (#19)"), + li(text: "**Grammar-inverse rows:** 1 committed / 3 in witness bundle / ~15 wave2a productions defined"), + ]), + h2(text: "4. Size call"), + p(text: "**LARGE multi-slice** — not a single row PR. Cheap tranche = grammar-row extensions (#17) + operator catalog derivation onto default TargetModel if row-only (#16). Load-bearing tranche = Match (#13) + loop/bind forms (#14–#15) + Branch (#18) — **HOLD for parent sign** before authoring TargetModel surfaces. Whole-tree tsc (#20) is terminal after per-construct gaps close."), + h2(text: "5. Sequencing (revised 2026-07-01)"), + 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_mvp1_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."), + ]), + p(text: "**Priority note:** Lane C is language-breadth; operator retains burn-down sequencing call. Proceed A → A2 → B meanwhile; HOLD D for both parent sign and operator priority."), + ] +} + +data typescript_gap_census_plan_doc_provenance: String = "bind: docs/plans/typescript-gap-census.md" + +data typescript_gap_census_plan: Plan = Plan { + slug: "typescript-gap-census", + title: "TypeScript first-class gap census — discriminating construct audit (Lane C / Track T)", + body: typescript_gap_census_body(), + dissolution: HasTrigger { + text: "Delete this census once every FAIL-OPEN row (#13–#20) is closed with execution-grounded witnesses and bar (c) tsc-green holds on the default TargetModel — the audit record is superseded by the substrate facts it enumerated." + } +} diff --git a/dsl/gunbc/plans/v2_self_hosting.dag b/dsl/gunbc/plans/v2_self_hosting.dag index 2ed960615e5..a2b4b6bceaa 100644 --- a/dsl/gunbc/plans/v2_self_hosting.dag +++ b/dsl/gunbc/plans/v2_self_hosting.dag @@ -19,13 +19,13 @@ fn v2_self_hosting_body() -> List { li(text: "**IMPROVED — the gap now has an owner and a construction-first fix.** The reconciliation endgame is **bright-stag-owned**: a model-first *single-authority* kill — **derive** the hand-maintained copy-lists FROM the emitted-module authority so the emitted↔hand drift becomes **unwritable** (the `invert-hand-maintained` move), with crisp-carp's `regen-verify` floor gate as the weaker post-hoc backstop layered on top. roadmap **`5-regen-verify` pulled forward**. cool-carp owns the *immediate* reconcile (fix the copy-lists + re-seed the 4 + verify clean) ahead of the construction fix."), li(text: "**IMPROVED — sequencing crystallized (emitter-first).** Order is now fixed: emitter-correctness settles (jolly-cat's Route-A lane; the corpus-emit surface measured at **~12,600 `E0308`**) → **single regen cutover** (bright-stag reconciliation) → `regen-verify` green → §7 fixpoint provable. Cutting over mid-emitter-churn re-drifts immediately, so the cutover is the *closing* step, not concurrent. This refines *Forced precondition order* step 3 below (it now has an owner + an ordering)."), li(text: "**DECIDED — open question #1 (reopen direction).** Resolved to **(a)**: finish the Route-A green bootstrap (continue `emitter/seed-green-integration`, do **not** restart into a pure-`.dag` coherence reset). Anchored; do not re-litigate."), - li(text: "**UNTOUCHED (still the wall, unchanged since 2026-06-21):** the Route-A last mile — the emitted crate still does **not** `cargo build` green (the `dsl_compile_clean` gate still only proves *well-typed*, not *built*). Track B / Stage C is still fail-closed (no real-digest match; comparison substrate still operator-pending, merry-crab-687). Track T (TypeScript) is still proven only on the `add` slice. The 590s+ whole-tree resolve is still the practical wall. None of these moved."), + li(text: "**LANDED — Route-A last mile (2026-06-25..28, #5777/#5873; re-verified cool-ant-875 2026-07-01).** `regen_stage0 --emit-fresh` → faithful assembled crate → `cargo build` debug+release is **0 errors** (`route_a_emit_fresh_cargo_green_test` witness). `dsl_compile_clean` still only proves well-typed emit (not built); the execution witness is the receipt. **Still open:** Track B / Stage C (no real-digest match; comparison substrate operator-pending, merry-crab-687). Track T (TypeScript) proven only on the `add` slice. The 590s+ whole-tree resolve is still the practical wall."), li(text: "**Tracked elsewhere (not a self-host milestone):** the CI-fleet resource problem (session over-allocation, CI-floor under-sharding, resolve-cache) → `compute-envelope-model.md`; the std fork census → `dsl-v2-defork-audit.md`. The session-spawn cap *was* fixed operationally 2026-06-23 (per-session RAM reservation 31g→4g, ~30 sessions/host) — an infra fix, orthogonal to this track."), ]), h2(text: "0. State of play (what's done, what's open)"), ul(items: [ li(text: "**Front-end — DONE, proven at scale.** `src/v2/` is 100% `.dag` (698 modules, 0 `.rs`; all Rust is the `src/v1` seed, ~154k lines). Full pipeline present: `01_tokenize → 02_parse → 03_resolve/name_resolve/ingest → 04_infer → 05_emit/eval → 06_translate → 07_target_carriers`. The historical blockers are fixed and merged: parse-perf (#5093 ParseTable memo, #3661), resolve/infer cost (#5258 the O(2^depth) double-resolve fix, #5266, #5146), cross-file names (#5271 Route C Phase B, #5154 filepath→QualifiedName). gap-4 (let-stmt in match arm) merged #5369; whole-tree parse-regression scanner added #5406. *Nuance:* per-file parse is fast, but a **combined `dsl`+`src/v2` whole-tree resolve is still heavy (590s+)** — \"no perf wall\" means the fixed blockers, not an instant full-tree resolve."), - li(text: "**Emit / Route A — runs whole-tree, but the emitted crate doesn't build yet.** `gunbc compile --source-root … --target rust` exists and the CI `dsl_compile_clean` gate runs it over `[src/v2, dsl]`, gating all of batch-2. **But the gate only proves the tree is well-typed** (emit runs to completion, writes `$OUT`, then `rm -rf $OUT`). It does **not** `cargo build` the emitted whole-tree crate. Only the emit-host MVP smokes compile tiny fixtures. **The green build of the emitted crate is the open Route-A last mile.**"), + li(text: "**Emit / Route A — whole-tree emit + faithful `--emit-fresh` crate builds green (#5777/#5873).** `gunbc compile --source-root … --target rust` exists and the CI `dsl_compile_clean` gate runs it over `[src/v2, dsl]`, gating batch-2 (well-typed emit only — writes `$OUT`, then `rm -rf $OUT`). The **cargo-green** receipt is `regen_stage0 --emit-fresh ` → `cargo build` (debug+release), proven by `route_a_emit_fresh_cargo_green_test`."), li(text: "**Fixed-point proof — fail-closed (not achieved).** `self_host.dag`'s `self_host_fixed_point_validate` **unconditionally returns `Rejected`** (`self_host_runner_not_realized`) — the honest contract until Stage C. `self_host_fixed_point_digests_match` (`==` over `content_hash`) is realized but de-risked only on fixture stages. The whole-compiler fixed point over real digests does not yet run."), li(text: "**Emitter — genuinely multi-target.** One `fold_node` catamorphism in `06_translate.dag`; emit selects a target's `target_model_edge_translation_rules` and walks the same rows **backward** (`grammar_relation_row_reverse_parse_selection`). 14 targets in `src/v2/extdeps/languages/` (rust, python, go, bash, dag, cpp, typescript, kotlin, swift, java, lean, ptx, verilog, …), 5 in `dsl`. A new target is **data rows, never a new emitter**."), ]), @@ -34,11 +34,11 @@ fn v2_self_hosting_body() -> List { p(text: "Get the v2-emitted Rust compiler to build and reproduce itself."), ol(items: [ li(text: "Emit whole tree `--target rust` — **done** (well-typed under CI gate)."), - li(text: "`cargo build` the emitted crate green — **open** (the last mile)."), + li(text: "`cargo build` the emitted crate green — **done** (#5777/#5873; `regen_stage0 --emit-fresh` witness)."), li(text: "`regen_stage0` from the emitted crate; replace the hand-Rust seed."), li(text: "Flip the lockstep / fixed-point gate from fail-closed to asserting the real `content_hash` digest match (Stage C)."), ]), - p(text: "Unmerged work: branch `emitter/seed-green-integration @ 239ff284d5` (**not in main**) carries 6 commits toward a green regen — import-completeness (E0425), List→host-`Vec`, Int-as-generic-arg→`i64`, `regen_stage0` patch, + 2 integration commits. PR **#5325 is CLOSED, not merged.** Recent emitter slices on main: #5413 (length→count, phantom-marker derives, Measure-alias E0560 peel, E0308 Box-deref cluster); MachineWidth is **#5397** (E0107), a separate PR."), + p(text: "**Route-A cargo-green landed on main** (#5777 emitter fixes → 0 rustc errors; #5873 two-generation regen cutover + `regen --verify` CI gate). Branch `emitter/seed-green-integration` content is absorbed — the branch is stale vs `main` and can be retired. PR **#5325** remains closed (superseded by #5873)."), h3(text: "Purity: no stage0 hand-edits (the requirement, and the enforcement gap)"), quote(blocks: [ p(text: "**UPDATE 2026-06-23 (#5639): this gap has now FIRED** — the seed has measurably drifted from the `.dag` (~764 regen errors, stale copy-lists). The \"erosion\" warned about below is no longer hypothetical. Owner + fix in the *Δ since 2026-06-21* block above."), @@ -46,10 +46,10 @@ fn v2_self_hosting_body() -> List { p(text: "The requirement — **v2 emits its own seed; no human stage0 patches** — is *modeled, currently unmet, and un-enforced.* `src/v2/workflow/bootstrap.dag` is the authority and states it exactly (\"seed→stage0→stage1→stage2, fixpt stage1==stage2 … seed used once; v2 is never in the loop again\", DESIGN §7), including the trust machinery to retire the seed (`SeedHonestyDischarge`, `DiverseCompilationAgreement`/`IndependentCompilerPair` = Diverse Double-Compiling, the Thompson trusting-trust defense). But:"), ul(items: [ li(text: "**The seed is hand-maintained today.** `regen_stage0.rs` carries `HAND_MAINTAINED_STAGE0_FILES` + `patch_*` (e.g. `patch_bootstrap_dag_collect`) that compensate for emitter gaps — each a \"stage0 hand-edit standing in for a thing v2 should emit itself,\" honestly marked with a dissolve-on pointing at the emitter fix. (Gotcha: regen has pre-existing codegen drift, so focused PRs hand-edit the `.rs` seed mirror rather than commit a full regen — itself a symptom of the gap.)"), - li(text: "**The no-drift gate is real but not wired.** `regen_stage0 --verify` (`verify_stage0_matches` — \"committed stage0 matches fresh self-compile\") exists, but a grep of the CI floor (`src/v2/workflow`, `dsl/tools`, `dsl/gunbc`, `dsl/test`) finds it nowhere. The `Stage0LockstepGate` that would wire it in is the content of **closed/unmerged #5325**. So hand-drift goes silently uncaught — erosion by one more honest-looking `patch_*` at a time."), + li(text: "**The no-drift gate is wired (#5873).** `regen_stage0 --verify` runs in the CI floor via `RegenVerifyGate` → `regen_verify_gate_passes` (`src/v2/workflow/ci_floor_plan.dag`). It enforces no drift on **generated** `GENERATED_STAGE0_FILES`; `HAND_MAINTAINED_STAGE0_FILES` are copied through by design. Closed #5325's `Stage0LockstepGate` was superseded by #5873. **Still open:** dissolve `patch_*` / hand-maintained copies so the emitter owns the whole seed (roadmap `5-dissolve-patches`)."), li(text: "**bootstrap.dag is 🟡 scaffold** — structural wiring only, placeholder hashes (dissolve-on T-15/T-20 `content_hash` supplying real per-stage merkle digests), so it does not yet *prove* convergence."), ]), - p(text: "**This gate is the keystone for both the purity requirement and a trustworthy cutover.** It is what makes \"no stage0 hand-edits\" enforceable; without it the requirement can only erode."), + p(text: "**The regen-verify gate is the keystone for a trustworthy cutover** — it now runs in CI (#5873), but hand-maintained seed copies and `patch_*` remain until `5-dissolve-patches` lands."), h3(text: "Track B — the fixed-point proof (Stage C)"), p(text: "`candidate_generation.dag` (`generate_stage_candidate_from_ingest`) drives `assemble_program_from_ingest → infer → translate`, capturing the emitted **Node** before `serialize_target` — the input Stage C needs. Comparison substrate (emitted Node vs emitted bytes) is operator-pending (merry-crab-687). When it lands, the fail-closed runner flips to `Accepted` + real-digest match. Proven **per realization** (Rust first; TypeScript once its target rows are complete)."), h3(text: "Track T — TypeScript as a first-class realization"), @@ -60,9 +60,9 @@ fn v2_self_hosting_body() -> List { p(text: "So \"delete stage0\" decomposes — `src/v1` also provides the **CLI bins** (`claim_executor`, `regen_stage0`, `yaml_check`, …), the **CI floor runner**, the **host-effect transports**, and the **evaluator that runs `.dag`**. Each must be v2-emitted or pinned *before* it can go; a big-bang `rm -rf src/v1` after a green fixed point would take out the execution substrate, not just the redundant compiler."), p(text: "**Forced precondition order (each gates the next):**"), ol(items: [ - li(text: "Whole-tree emit → `cargo build` green (Track A last mile)."), + li(text: "Whole-tree emit → `cargo build` green — **done** (#5777/#5873; `regen_stage0 --emit-fresh` witness)."), li(text: "Real fixed point: `self_host_fixed_point_digests_match` over real `content_hash` (Track B / Stage C; dissolve the placeholder hashes, T-15/T-20)."), - li(text: "`regen_stage0 --verify` green **and wired into CI** (the `Stage0LockstepGate`, closed #5325) + all `patch_*` / `HAND_MAINTAINED_STAGE0_FILES` dissolved so the emitter emits the whole seed. **This is the step that actually retires \"stage0 hand-edits\"** and makes the cutover trustworthy. *(Owner + ordering, per #5639: the single regen **cutover** is bright-stag-owned — derive the copy-lists from the emitted-module authority so the drift is unwritable — and lands **after** the emitter largely settles (jolly-cat's emitter-correctness lane), since each emitter fix shifts what a regen produces. crisp-carp's `regen-verify` floor gate is the backstop. roadmap `5-regen-verify` pulled forward.)*"), + li(text: "`regen_stage0 --verify` wired into CI — **done** (#5873 `RegenVerifyGate`) + all `patch_*` / `HAND_MAINTAINED_STAGE0_FILES` dissolved (**open**, roadmap `5-dissolve-patches`) so the emitter emits the whole seed. **This is the step that actually retires \"stage0 hand-edits\"** and makes the cutover trustworthy. *(Owner + ordering, per #5639: the single regen **cutover** is bright-stag-owned — derive the copy-lists from the emitted-module authority so the drift is unwritable — and lands **after** the emitter largely settles, since each emitter fix shifts what a regen produces.)*"), li(text: "Seed-honesty discharge (ideally via Diverse Double-Compiling)."), li(text: "Then collapse `src/v1` to the pinned reproducible seed and delete its compiler logic **incrementally** — verify by execution, not assumption."), ]),