Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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)

Expand Down
48 changes: 48 additions & 0 deletions docs/plans/disposition-carrier.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions dsl/gunbc/roadmap_authority.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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: [],
),
Expand All @@ -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")]),
],
Expand All @@ -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")]),
],
Expand Down