diff --git a/ROADMAP.md b/ROADMAP.md index 68544ad0260..6e5056ded2a 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -29,7 +29,7 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l - [x] **numeric-tower grounding** (#5428) — `Int=GroupCompletion`; `==` straddle guard now dead-in-corpus ([plan](docs/plans/model-realization-fork.md)) - [ ] **cache trustworthy** — authoritative home is §2 F2/F3/P1; ship the warm==cold oracle as a detective now -- [ ] **rust-gate coverage** (shared §1) — opt-level=3 restores Pop-A to per-PR (#5456); run-all-unless-`#[ignore]`d (#5427) ([cause table](docs/plans/expensive-test-cause-table.md)) +- [ ] **rust-gate coverage** (shared §1) — opt-level=3 restores Pop-A to per-PR (#5456); run-all-unless-`#[ignore]`d (#5427) ([cause table](docs/plans/ci-selection-vs-scheduling.md)) - [ ] **promote-or-delete every inert lens** + de-vacuum thin gates *(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)* @@ -45,6 +45,7 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l **Meta — lock down the reasoning (§7 recursion):** - [x] **inert-lens hygiene backstop** — every `lens/*.dag` wired or deleted; runs over the corpus (#5433) +- [ ] **reachability-completeness lens** — every declared node (code carrier · doc · lens) reachable from a run-root, rostered, or deleted; generalizes #5433 to carriers + docs ([plan](docs/plans/inert-layer-lens.md)) - [ ] **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) *(quick-ant-298)* - [ ] **construction-justification rule** (authoring-time) — justify why a class can't be construction before adding a lens ([DESIGN §6](DESIGN.md)) *(silent-wren-739)* - [ ] **expressibility frontier** — partition each modeling discipline into wall / lens-residue / undecidable-review *before* gating ([plan](docs/plans/expressibility-frontier.md)) diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md new file mode 100644 index 00000000000..36274b14836 --- /dev/null +++ b/docs/plans/inert-layer-lens.md @@ -0,0 +1,216 @@ +# The inert-layer lens — modeled but unreached + +> A lens that reports declared concepts (carriers, fns, whole modules) that are **modeled but unreached +> from any live run-root** — DESIGN §6's "the machinery exists but nothing gates on it," made +> *observable* and eventually fail-closed. The dangerous subset, and the reason for the lens, is the +> **load-bearing-but-unwired** layer: a richly-structured carrier that *looks* like it drives behavior +> and drives none. DESIGN refs: §3 (single authority — generalizes the #5433 inert-lens backstop, does +> not fork it), §5 (fail-closed; construction over validation), §6 (lens as residue; coverage-by-illusion), +> §7 (recursion — the compiler's own dead model is a substrate fact). + +## 1. The definition (why reference-count is not enough) + +A declared concept is **inert** iff it is **not reachable from a live run-root** over the reference +graph. The subtlety that makes this a real lens and not a grep: + +- **Reference-count overstates liveness.** A carrier with N>0 consumers can still be inert if all N + consumers are themselves inert — a self-referencing cluster. Measured example: `RealizationObjective` + and `ComputeOffer` each have 4 consumer files, but `RealizationObjective` is **live** (`ci_floor_plan`, + a run-root, imports `realization_width`→it) while the work-demand cluster around `ComputeOffer` reaches + nothing that runs. Same count, opposite verdict. **Reachability, not count.** +- **Run-roots ≠ test-roots.** The existing #5433 backstop seeds reachability from *discovered test + witnesses* — it answers "is this lens **covered**?". Inert-layer detection must seed from the *run* + roots — what actually executes in production: the CI floor plan, the compiler pipeline driver, the emit + entry. A module reached only by tests but by nothing that runs is *inert in production yet covered* — a + distinct, also-interesting state. The lens reports both, labeled. + +So: **inert = declared ∧ ¬reachable(run-roots)**. Decidable (graph reachability), a pure Node read. + +### 1.1 The rules — what is a hard wall, and what only looks like one + +Four cases decide whether this is a *rule* or a *vibe*. Each lands in a different frontier region +([expressibility-frontier](expressibility-frontier.md)); the design discipline is to keep them apart. + +- **Does a test consumer count? — NO, for the *live* verdict; it is a separate, labeled state.** Run + reachability from each root set independently: run-roots (executed entries) → "inert in production?"; + test-roots (witnesses) → "covered?". A concept reachable from tests but not from run-roots is + **"tested but unrun"** — its own bucket (a test can pin dead code alive). Report it; **wall only on + run-root-inert.** Decidable per root set → ①. + +- **One consumer, but that consumer is dead? — you never count local consumers.** The verdict is + *membership in the complement of the reachable set*, a fixpoint from the roots over the whole tree. A + node alive only through a dead consumer is simply not in the reachable set → inert. "Inspect the entire + tree" is exactly right: global reachability, not per-node degree. This is the case reference-count gets + wrong (§1). Decidable → ①. + +- **Dead arms / fields (one honest reading of "should be 10, has 1") — decidable, a sharper wall.** A + reachable carrier can still have *arms never constructed* or *fields never read*. Arm-level + reachability is decidable (an arm appears in some reached construction or it doesn't), and the *match* + side is already CoproductExhaustiveness (§4 testgen). So "a 6-arm coproduct where 3 arms are never + built" is a wall, not a guess → ①. + +- **One consumer, but it *should* be ten call-sites? — this is NOT inertness, and forcing it into this + rule breaks the wall.** "Should be ten" needs the set of sites that *ought* to consume the concept — + not derivable from the concept alone (③ undecidable directly, by Rice). But its **dual is decidable**: + the sites that should have consumed an authority and didn't are the ones that *rolled their own + equivalent* — a §3 nickname / §2 anemic pattern. So under-consumption is detected **as redundancy**, by + the anemic / nicknaming lens, *not* by counting expected consumers. + +**The framing rule: inertness (0 reachable) is a wall; under-wiring (too few) is a hand-rolled fork — +keep them separate.** Fusing them is the trap: you would try to make "should be N" a hard gate, fail by +Rice, and either fire falsely or abandon the whole rule. + +So the hard rule is exactly the **0-reachability** one, and it is a wall on three conditions: +1. **the run-root set is enumerable** — it is (the floor plan, the compiler/emit drivers, the CLI bins: + things with a `main` or a discovered entry). A fuzzy root set is a fuzzy wall — pin it. +2. **reflective / host-bridge consumption counts as an edge** — `concept_index` is host-fed and the floor + discovers witnesses by marker scan, not import; a carrier consumed only through such a bridge is + *live* and would false-positive a pure import walk. The roots must include the bridge entry points. +3. **a named, shrinking exception roster** for carriers deliberately modeled ahead of their consumer (the + realization loop is model-first by design) — each entry names its dissolve-on PR; the roster empties + as the loop wires them, and the lens flips advisory → wall when it does (the #5433 / realization-vocab + shape). + +The rule, stated once: + +> A declared concept must be **reachable from a live run-root** (over static **and** reflective edges), +> be on the **exception roster** with a dissolve-on, or be **deleted**. Test-only reachability is a +> separate "unrun" bucket — reported, not gated. **Under-consumption is out of scope** — it is the +> redundancy lens, not this one. + +## 2. The census (the discriminating witnesses the lens must reproduce) + +Measured 2026-06-21 over `dsl/**` + `src/v2/**`, reachability cross-checked against run-roots +(`ci_floor_plan`, `scheduler`, the v1 run path). This is what the lens must independently re-derive: + +**Fully inert (0 live consumers), load-bearing — the target class:** + +| carrier | home | what it models | +| --- | --- | --- | +| `CacheLayerPlan` | `cache_interface.dag` | the L1/L2/L3 cache-layer plan — the whole §2 cache-planner output | +| `WorkDemand` | `compute_fabric.dag` | the work-demand vocabulary (isolation/memory/GPU) — nothing emits one | +| `ParallelismShape` · `IndependentShards` · `PartitionedReduce` | `compute_fabric.dag` | the corpus-sharding demand model | +| `Partitioner` · `SymbolicCost` (forward-stubs `= Node`) | `compute_fabric.dag` | map→reduce execution decomposition | +| `execution_receipt_digest` | `compute_fabric.dag` | the digest the 3-dimension unification rests on — a stub returning `work.id`, consumed nowhere | + +**Edge-wired (consumed by a model that is not itself the live source yet):** + +| carrier | consumed by | why still inert-at-the-edge | +| --- | --- | --- | +| `ComputeOffer` / the fleet model | `ci_fleet`, `operator_fleet`, `runner_spec_from_offer` | projected to a `RunnerSpec`, but `ci.yml`'s runner block is still a literal — the projection isn't the live emission source (Phase 3 open) | + +**Now-wired (recorded so the lens does *not* false-positive these):** + +| carrier | reached via | +| --- | --- | +| `RealizationObjective` · `realization_width` · `HardwareThreadCount` (11) · `AxisGoal` | `ci_floor_plan` → `realization_width.width_fold_objective_goals` / `memory_aware_spawn_width` — the memory-aware width landed; the *schedule/width* arm of realization is live | + +The reading: the **schedule/width** arm of the realization layer is now wired; the **cache-plan** arm and +the **work-demand / sharding / receipt-digest** arm are the inert load-bearing layers. Exactly the +realization-loop thesis ("shape-complete but input-starved"), now with names. + +## 3. Two tiers (what's buildable now vs gated) + +**Tier 1 — module-level, buildable now (reuse #5433).** `inert_lens_modules` (`cli_run.rs:2558`) already +computes module-import transitive closure from seed roots and reports unreached `v2.lens.*` modules. The +inert-*layer* lens is the **same machinery with two generalizations**: (a) widen the output filter from +`is_top_level_lens_module` to *all* modules; (b) seed from the **run-roots** (floor plan + pipeline + +emit), not only discovered witnesses. Output: unreached *files/layers*. Reuses the existing BFS over +`module_to_path` + `path_imports`; no new host machinery. + +**Tier 2 — symbol-level, gated.** Within reached modules, which declared carriers/fns have zero live +consumers (the §2 census above is symbol-level). This needs **whole-corpus reference (`BindsTo`) +enumeration**, which does *not* exist today — `dependency_lens` is per-declaration, `concept_index` +enumerates *declarations* but not *reference sites*. So Tier 2 is host-fed today (a +`enumerate_all_binds_to_edges()` bridge beside `concept_decl_facts_live()`) and becomes a pure `.dag` +walk on the **same dissolution trigger as `concept_index`** (gunbc#5364 — v2 self-host gains +compile-graph access). Until then Tier 2 is host-fed, Tier 1 is pure. + +## 4. The load-bearing ranking (the advisory half) + +"Inert" is decidable; **"load-bearing" is a heuristic** — so the lens *decides* inertness and *ranks* +apparent load-bearingness, never gates on the ranking. Rank an inert concept by structural richness: +coproduct arm-count + record field-count + fn return-type richness, plus name signals +(`Plan`/`Account`/`Receipt`/`Schedule`/`Demand`/`Policy`). A 6-arm `ParallelismShape` with 0 consumers +ranks far above an unused 1-line helper. This is the operator's exact ask — "ones that *seem* load-bearing +but are unwired" — surfaced as the ranked head of the inert list. + +## 5. Frontier placement (per [expressibility-frontier](expressibility-frontier.md)) + +- **Inertness is a ① wall candidate.** Reachability is decidable; an inert load-bearing carrier should + eventually **fail closed** exactly as #5433 does for lenses ("an inert lens is a lie" → "an inert + load-bearing carrier is a lie"). The honest path: ship as a ② *observing* lens first (a ranked report, + no gate), promote to a ① wall once the corpus is clean enough that a new inert load-bearing carrier is + a genuine defect rather than expected staged-ahead modeling. +- **The "staged-ahead" exception is the catch.** Much of the inert set is *deliberately* modeled before + its consumer (the realization loop is built model-first by design). So a blanket wall would fight the + project's own just-in-time-after-modeling discipline. The resolution is the #5433 pattern: a + **named, shrinking exception roster** (carriers modeled ahead of a tracked consumer-PR) that empties as + the realization loop wires them — the same ratchet-during-migration → wall-when-empty shape as the + realization-vocabulary guard. Each roster entry names its dissolve-on (the PR that wires it). +- **The ranking is the ② residue**, permanently advisory (judging "load-bearing" needs domain knowledge). + +## 6. Reuse map (do not fork — §3) + +| need | reuse | file | +| --- | --- | --- | +| transitive reachability BFS | `inert_lens_modules` | `cli_run.rs:2558-2606` | +| enumerate all declared concepts | `concept_index.enumerate_concepts()` | `concept_index.dag:130` | +| use vs structural edge classification | `unused_parameters` `UseRelation` (`BindsTo` = the use authority) | `unused_parameters.dag:22` | +| import/reference edge-walk | `layering_imports` projection | `layering_imports.dag` + `layering_imports_project.rs` | +| run-roots | floor gates + corpus + pipeline/emit entries | `ci_floor_plan.dag:83`, `cli_run.rs:run_discovery_corpus` | + +## 7. Wiring + dissolution + +- Tier 1 lands as `v2.lens.inert_layer` + a floor witness; runs over the corpus, **reports** (advisory) + first, ranked, with the exception roster. +- Promote to fail-closed once the roster is small and stable (per §5 above). +- **Load-bearing seed caveat:** Tier 1 touches `cli_run.rs` (the #5433 closure) — a DESIGN-named + load-bearing file → **escalate before editing**; prefer extending `inert_lens_modules` behind a flag to + forking it. +- **Dissolution:** the lens itself never dissolves (inertness is a standing property); its *exception + roster* dissolves to empty as the realization loop wires each carrier, at which point the lens flips + from advisory ② to fail-closed ① wall. + +## 8. Generalization — one rule, N substrates (code · docs · lenses) + +Reachability-completeness is **not specific to code** — it is a §2-horizontal "one concept, every +breadth": *every declared node in a graph must be reachable from a root, on an exception roster, or +deleted.* It already runs over the **lens** graph (#5433). It applies unchanged to the **doc** graph — +and the doc instance is the **cheapest wall of all** (pure link reachability, no reflective edges, no +host bridges): + +| substrate | nodes | edges | roots | inert = | dangling = | +| --- | --- | --- | --- | --- | --- | +| code | declared concepts | reference / `BindsTo` | run entries | unreachable carrier | — | +| **docs** | `docs/**/*.md` | markdown links (+ `.dag`-comment `bind:` refs) | `ROADMAP.md`, `DESIGN.md`, runbook index | **orphan plan doc** | **broken `](path)` link** | +| lenses | `v2.lens.*` | module imports | discovered witnesses | inert lens (#5433) | — | + +The same three conditions (§1.1) decide the doc wall: +1. **enumerable roots** — `ROADMAP.md` + `DESIGN.md` for *plan* docs; **runbooks need their own root** (an + operational index), or they false-positive (a runbook is not a roadmap item). Pin the root per doc + *kind*. +2. **reflective edges count** — a doc referenced only from a `.dag` comment (`bind: docs/...`, the + CLAUDE.md open thread) is *consumed* but invisible to a markdown-link walk; include those refs. +3. **exception roster** — best expressed as a **PR-local rule**: a PR that adds `docs/plans/X.md` must add + its inbound link in the same PR. That is the doc-graph analog of "an inert lens is a lie" — and this PR + honors it (it adds this doc *and* its ROADMAP line). + +**Live census (2026-06-21) — the doc instance's discriminating witnesses:** 18 docs, 13 reachable, +**5 orphans** — `compile-clean-forcecheck.md`, `inert-layer-lens.md` (this very doc, before its ROADMAP +line landed — the self-demonstrating case), `m4-universal-hermetic-corpus.md`, +`m5-fixture-store-consolidation.md`, `runbooks/bmc-redfish-operator-access.md` (likely a legitimate +runbook-root case, not a roadmap orphan) — and **1 dangling link**: `ROADMAP.md`'s rust-gate-coverage +bullet linked `docs/plans/expensive-test-cause-table.md`, a #5463 forward-reference never written (the +Pop-A/Pop-B content already lives in `ci-selection-vs-scheduling.md`, so a new doc would §2/§3-duplicate +it). **Repointed in this PR** to the doc that holds the content. The wall would have blocked all six. +(Methodology note: the *first* census run reported this ref as 2× — it had read a stale local `ROADMAP` +behind main's terse pass; the lens must run against the live tree, the same discipline it enforces.) + +## 9. Open + +- Confirm the run-root set (is `scheduler.dag` the sole runtime, or also the v1 `claim_executor` path? + the digest census touched both). +- Decide Tier-1-now vs wait for Tier-2's host bridge so the first landing is symbol-granular (the census + shows the interesting cases are symbol-level — `execution_receipt_digest`, `CacheLayerPlan` — so a + module-only first cut may under-deliver; weigh against Tier 1's zero-new-machinery cost).