diff --git a/ROADMAP.md b/ROADMAP.md index 347e9d32724..dde92cb4d21 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -57,13 +57,13 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l - [ ] **promote-or-delete inert lenses · de-vacuum gates** — EmitHostGate de-vacuumed ✓ (#5477); 4 advisory lenses widened+bounded, whole-corpus deferred to `.dag` structural-reflection (also unlocks coverage/testgen) *(silent-wren-739)* - [x] **realization-vocabulary containment guard** (#5445/#5453) — target-AST importable only at the realization edge (fail-closed, shrinking-roster); dissolve-on: bash-sidecar arc empties the roster → pure wall → `program.dag` deletable [plan](docs/plans/emission-ingestion-inverse.md) - [ ] **stage0 clone-census inert + seed regressed** to 21540 (~1138 over) — resolve by clone-reduction / substrate-migration, NEVER a cap-bump; #5427 `#[ignore]` is the interim *(fierce-hawk-540 via quick-ant-298)* +- [ ] **`Disposition` carrier** *(un-parked, operator GO)* — slice-1 prove-by-use active *(adhoc-0a633bef-bb9 / fierce-crane-13 under neat-dove-397)*: model `Disposition`+`ConstructionMechanism` in std → migrate one region (the post-#5579 `data:String` marker fleet) → fail-closed redundancy lens. Single-authority convergence home for scaffold/rationale/dissolution marks; substrate-mandatory #1 is the end-state, not this slice. [plan](docs/plans/disposition-carrier.md) **Fenced OUT (after stability):** - [ ] **split `Value::Null`** (None/Absent/miss/Violates → own carriers) — ~131-site substrate change, the deeper root; own runway - [ ] **self-host purity gate** — a §5 deliverable, not §0 (avoids the §0↔§5 cycle) - [x] **cross-tree import activation** (§5) (#5473) — LANDED; the §0↔§5 escalate item is now closed -- [ ] **`Disposition` carrier** — a new concept; parked [plan](docs/plans/disposition-carrier.md) - [ ] complexity-budget whole-codebase (§3) · cache-redundancy completeness (§2 P3) — residue, after construction - [ ] **cardinality refinement** — illegal cardinalities (wrong length · empty · overflow) unwritable by construction; the *decidable* refinement axis (linear arithmetic over counts), fold-propagated. MVP-1 (`Byte` via `Length<8>`) + P4 (fold homomorphism · uint8 overflow → typed `Rejected`) proven (#5512); P1 (`where` lowering) / P2 (construction-enforced) behind this lane; P5 (phantom-width reflection) substrate-blocked. [plan](docs/plans/cardinality-refinement.md) [P1](docs/plans/p1-where-clause-lowering.md) @@ -74,7 +74,7 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l - [ ] **gate-hygiene: a floor-enrolled gate must be green-on-main at merge** — roster-completeness assertion promoted to should-land ([plan](docs/plans/emission-ingestion-inverse.md) §2; [merge-freshness decision record](docs/plans/ci-merge-freshness.md)) *(quick-ant-298)* - [x] **construction-justification rule** (#5476) (authoring-time) — justify why a class can't be construction before adding a lens *(silent-wren-739)* [plan](docs/plans/construction-justification-rule.md) [DESIGN §6](DESIGN.md) - [ ] **expressibility frontier** — partition each modeling discipline into wall / lens-residue / undecidable-review *before* gating [plan](docs/plans/expressibility-frontier.md) -- [ ] **confront the skipped modeling decisions** — the `🟡` comment backlog [Disposition plan](docs/plans/disposition-carrier.md) +- [ ] **confront the skipped modeling decisions** — the `🟡` comment backlog *+ the post-#5579 `data:String` marker fleet* (the comment-wall moved marks comments→rows, growing the §3-migrate surface); converges on the `Disposition` carrier (single authority, `0-disposition`) [Disposition plan](docs/plans/disposition-carrier.md) - [ ] **axiom + syllogism lens** (DESIGN open thread #1) — every claim chains back to an axiom, no orphan/cycle; stays `[ ]` until it runs executably over this doc [scope](docs/plans/axiom-syllogism-lens.md) - [ ] **self-applying lenses (detect → generalize → emit → write)** — a lens *produces the correct pattern and applies it via the write API*, not just flags; the §7-recursion upgrade to the whole lens family, unified by **redundant intent** (specification complexity above the essential min). Anti-unification is the shared engine (term-layer fold + `structural_similarity` type-generic = one kernel, two binders); seeded in `v2.lens.simulated_relationship` (#5584). Decidable-wall classes only — ratchet residue stays detect-only. Depends on §6 emit + a write effect + resolve facts [plan](docs/plans/self-applying-lenses.md) diff --git a/docs/plans/disposition-carrier.md b/docs/plans/disposition-carrier.md index 466d50dafc5..b0cd85ba855 100644 --- a/docs/plans/disposition-carrier.md +++ b/docs/plans/disposition-carrier.md @@ -23,6 +23,30 @@ convention standing where necessity was available). There is also no typed carrier: `Terminal`/`Scaffold` are text only; `src/v2/lens/registry.dag` lists lenses (`LensRegistryEntryV0`) for **9 of ~35** files with no disposition field. +### 0a. Post-#5579 reframe — the wall moved the ball halfway *and* grew the surface + +The comment-ban wall (#5579, `//` is now a parse error) changed the shape of this problem, it did not +solve it. The marks that used to live in comments were forced **out of comments and into `data: String` +rows** — `bytes_seam`, `unit_must_run_staged_note`, the Anthropic closure rows, the budget-tree leaves, +`consumed_input_closure_concept_note` / `_convergence_candidate` / `_slice1_status` (#5605). So the +problem statement is no longer "disposition lives in **comments** (invisible to a lens)" but +"disposition lives in `data: String` **rows** — **visible** to a lens as a Node, but still **opaque +prose** whose *meaning* a lens cannot read." Net: the wall made the marks Nodes (a lens can now *see* +them) but the §3-migrate surface **grew** to include the whole post-wall `data:String` fleet on top of +the original `🟡` extdeps comments. That **strengthens** this carrier's case — the displaced cost it +removes is now bigger and concrete, with named instances (§6: denominate the benefit). It does not +change the carrier: `data:String` prose → typed `Disposition` is the same move, with a larger, +already-Node-shaped input set. + +This is the chosen first proof-by-use region: **slice-1** (operator GO 2026-06-23, work-item +`adhoc-0a633bef-bb9`, `fierce-crane-13` under `neat-dove-397`) models `Disposition` + +`ConstructionMechanism` in `std` (a DESIGN-named load-bearing carrier → **checkpoint** to +`bright-stag-194` before any row migrates), migrates **this** `data:String` fleet region-by-region (each +region red-on-revert so the lens is never inert mid-migration), and lands the fail-closed redundancy +lens green-by-execution with a discriminating control. The substrate-mandatory **#1** end-state stays +the named goal, not this slice — slice-1 *proves the binary taxonomy by use before cementing it* +(see §2a). + ## 1. The carrier — one concept, two carriers (§2 horizontal, single authority) Lens-lifecycle tags and coproduct dissolve-markers are the **same concept**. One typed carrier: @@ -51,6 +75,30 @@ require the tag at definition, the lens is dead code and **dissolves**. The enfo disposed of *by* the discipline (same shape as the numeric-tower guard going dead). Jumping straight to #1 is rejected only on sequencing (substrate change + flag-day + unproven taxonomy), not on principle. +### 2a. Taxonomy stress-test — the hypothesis slice-1 must try to falsify + +The first real test input is #5605's `ConsumedInputClosure`, which appears to wear **three** dispositions +at once: the concept is sound (`_concept_note`), the impl is a scaffold (`_slice1_status`), and a +convergence is pending (`_convergence_candidate`). This *looks* like the binary `Terminal | Scaffold` is +too narrow and needs a soundness/completeness/convergence **axis split**. It is not — and that is the +ruling slice-1 carries in as a hypothesis to **falsify**, not a blank: + +- It is **N marks per carrier, not N axes per `Disposition`.** Those three are three *distinct* + `data:String` rows, each cleanly one disposition: `_concept_note` → `Terminal{reason}` (consume-input + vs produce-artifact is a permanent §3 distinction — the concept stays); `_convergence_candidate` → + `Scaffold{dissolves_to: the one selection authority all consumers reach}`; `_slice1_status` → + `Scaffold{dissolves_to: per-unit selection}`. (Convergence-pending *is* a `Scaffold` — "these N + authorities should become 1" is a §3 redundancy that dissolves when the merge lands — not a third + axis.) +- Splitting `Disposition` into axes would **grow the concept** to model what multiple-marks-per-carrier + already expresses (§2: net concepts must not grow by re-invention) — a failed decomposition. +- **The discriminating test:** can every mark be assigned *exactly one* `Disposition` without losing + information? If yes, the binary holds and the multiplicity is just per-carrier mark count. The + taxonomy needs the split **only** if a *single, indivisible* mark genuinely needs two dispositions at + once (sound-concept AND scaffold-impl fused in one row that cannot be split into two marks) — and + green-by-execution would then show it. Until a mark fails that test, the binary is the cheaper, more + grounded answer. + ## 3. What is actually enforceable (construction vs lens vs retro) - **Presence of a disposition** — *construction.* Non-optional field on the carrier ⇒ you cannot author diff --git a/dsl/gunbc/roadmap_authority.dag b/dsl/gunbc/roadmap_authority.dag index e1421548c64..93a66ea669e 100644 --- a/dsl/gunbc/roadmap_authority.dag +++ b/dsl/gunbc/roadmap_authority.dag @@ -79,6 +79,7 @@ fn section_0() -> RoadmapSection { derivable_doc(id: "0-realization-vocab", prs: [5445, 5453], title: "**realization-vocabulary containment guard**", description: "— target-AST importable only at the realization edge (fail-closed, shrinking-roster); dissolve-on: bash-sidecar arc empties the roster → pure wall → `program.dag` deletable", path: "docs/plans/emission-ingestion-inverse.md"), authored(id: "0-stage0-census", done: false, content: "**stage0 clone-census inert + seed regressed** to 21540 (~1138 over) — resolve by clone-reduction / substrate-migration, NEVER a cap-bump; #5427 `#[ignore]` is the interim *(fierce-hawk-540 via quick-ant-298)*"), + authored_doc(id: "0-disposition", done: false, content: "**`Disposition` carrier** *(un-parked, operator GO)* — slice-1 prove-by-use active *(adhoc-0a633bef-bb9 / fierce-crane-13 under neat-dove-397)*: model `Disposition`+`ConstructionMechanism` in std → migrate one region (the post-#5579 `data:String` marker fleet) → fail-closed redundancy lens. Single-authority convergence home for scaffold/rationale/dissolution marks; substrate-mandatory #1 is the end-state, not this slice.", path: "docs/plans/disposition-carrier.md"), ], edges: [], ), @@ -89,7 +90,6 @@ fn section_0() -> RoadmapSection { authored(id: "0-selfhost-purity", done: false, content: "**self-host purity gate** — a §5 deliverable, not §0 (avoids the §0↔§5 cycle)"), derivable(id: "0-cross-tree", prs: [5473], title: "**cross-tree import activation** (§5)", description: "— LANDED; the §0↔§5 escalate item is now closed"), - authored_doc(id: "0-disposition", done: false, content: "**`Disposition` carrier** — a new concept; parked", path: "docs/plans/disposition-carrier.md"), authored(id: "0-complexity-residue", done: false, content: "complexity-budget whole-codebase (§3) · cache-redundancy completeness (§2 P3) — residue, after construction"), authored_pp(id: "0-cardinality", done: false, content: "**cardinality refinement** — illegal cardinalities (wrong length · empty · overflow) unwritable by construction; the *decidable* refinement axis (linear arithmetic over counts), fold-propagated. MVP-1 (`Byte` via `Length<8>`) + P4 (fold homomorphism · uint8 overflow → typed `Rejected`) proven (#5512); P1 (`where` lowering) / P2 (construction-enforced) behind this lane; P5 (phantom-width reflection) substrate-blocked.", carriers: [ptr(label: "plan", path: "docs/plans/cardinality-refinement.md"), ptr(label: "P1", path: "docs/plans/p1-where-clause-lowering.md")]), ], @@ -105,7 +105,7 @@ fn section_0() -> RoadmapSection { derivable_pp(id: "0-construction-rule", prs: [5476], title: "**construction-justification rule**", description: "(authoring-time) — justify why a class can't be construction before adding a lens *(silent-wren-739)*", carriers: [ptr(label: "plan", path: "docs/plans/construction-justification-rule.md"), ptr(label: "DESIGN §6", path: "DESIGN.md")]), authored_doc(id: "0-expressibility", done: false, content: "**expressibility frontier** — partition each modeling discipline into wall / lens-residue / undecidable-review *before* gating", path: "docs/plans/expressibility-frontier.md"), - authored_pp(id: "0-skipped-modeling", done: false, content: "**confront the skipped modeling decisions** — the `🟡` comment backlog", carriers: [ptr(label: "Disposition plan", path: "docs/plans/disposition-carrier.md")]), + authored_pp(id: "0-skipped-modeling", done: false, content: "**confront the skipped modeling decisions** — the `🟡` comment backlog *+ the post-#5579 `data:String` marker fleet* (the comment-wall moved marks comments→rows, growing the §3-migrate surface); converges on the `Disposition` carrier (single authority, `0-disposition`)", carriers: [ptr(label: "Disposition plan", path: "docs/plans/disposition-carrier.md")]), authored_pp(id: "0-axiom-lens", done: false, content: "**axiom + syllogism lens** (DESIGN open thread #1) — every claim chains back to an axiom, no orphan/cycle; stays `[ ]` until it runs executably over this doc", carriers: [ptr(label: "scope", path: "docs/plans/axiom-syllogism-lens.md")]), authored_pp(id: "0-self-applying-lenses", done: false, content: "**self-applying lenses (detect → generalize → emit → write)** — a lens *produces the correct pattern and applies it via the write API*, not just flags; the §7-recursion upgrade to the whole lens family, unified by **redundant intent** (specification complexity above the essential min). Anti-unification is the shared engine (term-layer fold + `structural_similarity` type-generic = one kernel, two binders); seeded in `v2.lens.simulated_relationship` (#5584). Decidable-wall classes only — ratchet residue stays detect-only. Depends on §6 emit + a write effect + resolve facts", carriers: [ptr(label: "plan", path: "docs/plans/self-applying-lenses.md")]), ],