diff --git a/DESIGN.md b/DESIGN.md index 2bf6c59f6c8..b002e856994 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -114,7 +114,7 @@ The same arm exists at authoring time: **the workaround — an absorbing fallbac - **Model:** DFS the concept DAG before inventing vocabulary; fact-bundle modeling (invent or reuse on proven coincidence, never bare-alias); a finished stage is one fold (any non-fold residue is either a named irreducible kernel or un-migrated modeling — there is no third); model just-in-time and let the mark on the carrier be the authority (no parallel-ledger docs); **no scaffold lands by author declaration alone** — every net-new scaffold is represented by one exact dissolution obligation, joined to an external operator verdict on the current head, and refused in its absence (§5); reviewers independently search for undeclared scaffolds, so the author's classification is evidence to inspect, never the denominator. - **Intellectual sustainability:** don't spend future author, reviewer, operator or maintainer time to buy present convenience. Work expected to be thrown away is *presumed redundant* (§2), so back up and complete the construction that will survive; use a temporary one only after the operator explicitly chooses that future cost. The reviewer's independent test, applied whether or not the author labelled anything: **will this artifact survive the terminal architecture substantially unchanged, and be consumed by it?** If no, presume scaffold and stop the merge until the final construction lands or the operator approves the exact exception. A *missing* dissolution condition makes the finding **more** severe, not less — the response is to name the undeclared dissolvable concept, request the final architecture, and require the exact obligation model if the author believes an exception is warranted; adding a trigger after review does not resolve the objection, it only makes the proposal eligible for a decision. Automated detection can never be the whole policy, because temporary work can be authored without using any of the names a gate matches on. Tells, each carrying a presumption: a hand-authored workflow, deployment script, migration script or operational command (out-of-band actuation); a second path beside an existing modeled route (parallel authority); "bridge", "shim", "compatibility", "for now", "temporary", "until", "later" (deferred refactor); a model to be deleted whole when the real one lands (throwaway model); a hand-authored projection the model should generate (manual application committed as source); raw shell implementing semantics already expressible in `.dag` (unmodeled realization); a broad wrapper around a type or modeling deficit (workaround hiding substrate work); a condition whose terminal is "rewrite this properly" (the proper work was not done); a new artifact with no final consumer (experimental residue). If dissolution approvals become frequent, that is not a process cost to optimize away — it is evidence the repository is routinely borrowing future intellectual labor to ship present convenience. - **Prioritize holistically, not by the bottleneck:** balance the quantitative and the qualitative — don't anchor on one KPI (you'll hit it at a cost) or on pure taste. Map the cause→effect across sections; a 5ms step doesn't get a pass for not being the 80s one (it might be a 5ns step). One consequence is a standing rule, **bare minimum cost** (operator ruling 2026-07-10): a proven cost-shape defect — a copied accumulator, a quadratic fold — is *always fixed*, regardless of the realized n. "n is small here" is not a time-stable fact (§1/A3 — reuse changes n), and pricing per-site exceptions is itself redundant work (§2); the humility is not trusting your own "negligible here." Root-cause to the language layer and fix related systems *together* — a local subsystem patch is the forked-logic trap. **Denominate the benefit:** the deliverable is a *displaced cost* (§1's time — a pain someone pays to remove); the lens/substrate is the *mechanism* (the moat), not the product. A lens — or any construction wall — is on-dial exactly insofar as it is the cheapest path to such a pain. Priced in elegance instead, the work is self-referential and unbounded (the purity trap — the economic twin of "never" in §5; an extensible substrate's infinite improvability dissolving its own bound). -- **Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie, so an **executable** hygiene check must keep every lens either wired (a discovered fail-closed witness) or deleted — that backstop runs over the corpus and is *not* superseded by the authoring-time construction-justification judgment, which layers on top of it. +- **Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie. **The corpus-wide backstops that used to police this are DELETED (2026-08-11), and the reason is the rule that replaces them:** the inert-lens reach census and the construction-justification census both ran inside floor witness discovery, so *every* discovery run — on every PR, on regen, in every coordinated worker — had to acquire a whole-corpus module graph in order to answer a question about who authored a lens. That is the §6 cost-shape defect at its purest: the unit of computation was the world, the unit of fact was one module's authorship, and the price was paid by every consumer that wanted a witness roster and nothing else. **Who paid it, split by era, because this document must not assert a superseded population as the present one:** before #8140 the walk was unconditional, so ordinary CI, regen, the falsifier cadence and every coordinated worker all paid; #8140 made it demand-directed, so a discovery-free plan such as regen stopped paying; from #8140 to this deletion the two censuses burdened every remaining discovery-bearing execution. The correction is recorded rather than reworded because a change deleting stale supply-side enforcement must not land a fresh stale assertion in the same diff (review on #8141). Neither census had a consumer that justified the acquisition; the inert-lens half additionally reported through two host builtins whose `.dag` surface was a pair of self-recursive stubs (`fn f() { f() }`) reachable only because the interpreter intercepted them. **What is NOT claimed:** this is a real scope narrowing, not a climb. A newly authored lens with no witness, and a lens recording no `construction_justification`, are both writable again and nothing detects either. The obligation survives as review diligence, which is strictly weaker. **Next-rung trigger:** an authorship fact belongs on the module's own declaration, checked at ingestion where the module is parsed anyway — one module's facts from one module's source — rather than reconstructed corpus-wide by a consumer that wanted something else. Until that lands the class sits at *mitigatable*, declared here rather than left to be rediscovered. - *e.g.* one catamorphism `fold_node` is reused by all 7 v2 stages; #4699 dissolved `06_translate` 4,912→3,973 lines (`_go` accumulators 35→0); a 6-line `merge_envs` root fix cut reconcile from 81% of the pipeline to 6% (~2× self-compile) — the symptom recurs wherever the root is unfixed (v2 still hand-rolls `ParseTable` because the Realization carrier is staged, not inhabited). ## 7. Self-hosting (the principles applied to the compiler itself) diff --git a/dag/gunbc/cli_run_floor_lens_oracle_scaffold.dag b/dag/gunbc/cli_run_floor_lens_oracle_scaffold.dag index 62d28c3aa94..99c7d17b21e 100644 --- a/dag/gunbc/cli_run_floor_lens_oracle_scaffold.dag +++ b/dag/gunbc/cli_run_floor_lens_oracle_scaffold.dag @@ -3,44 +3,6 @@ module gunbc.cli_run_floor_lens_oracle_scaffold import std.dissolution { DissolutionCondition, dissolution_description, unbound_dissolution } -data cli_run_floor_lens_legacy_graph_oracle_scaffold: Disposition = Scaffold { - dissolves_to: SingleAuthority, - bind: DeclarationRef { - module_path: "v1_compiler.cli_run", - decl_name: "floor_lens_graph_legacy", - field: WholeDeclaration - } -} - -data cli_run_floor_lens_legacy_walk_oracle_scaffold: Disposition = Scaffold { - dissolves_to: SingleAuthority, - bind: DeclarationRef { - module_path: "v1_compiler.cli_run", - decl_name: "inert_lens_modules_legacy", - field: WholeDeclaration - } -} - -data cli_run_floor_lens_oracle_dissolve_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: floor_lens_graph_legacy + inert_lens_modules_legacy — the 6A repoint's TEST-SIDE equality oracle (the deleted build_floor_lens_import_graph corpus scan and module-name-grain walk, retained only inside cli_run.rs inert_lens_hygiene_tests as the executing equivalence receipt, the same shape as resolve_transitively_bfs_legacy). DELETES WHEN the legacy-oracle class dissolves (the queued resolve_transitively_bfs_legacy triage deletion) OR cli_run.rs Chunk F retires the HAND census entirely (docs/plans/cli-run-reconcile-defork.md)") - -data cli_run_floor_lens_census_walk_hand_rust_scaffold: Disposition = Scaffold { - dissolves_to: SingleAuthority, - bind: DeclarationRef { - module_path: "v1_compiler.cli_run", - decl_name: "inert_lens_modules", - field: WholeDeclaration - } -} - -data cli_run_floor_lens_justification_hand_rust_scaffold: Disposition = Scaffold { - dissolves_to: SingleAuthority, - bind: DeclarationRef { - module_path: "v1_compiler.cli_run", - decl_name: "lens_justification_census", - field: WholeDeclaration - } -} - data cli_run_floor_lens_read_refusal_hand_rust_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, bind: DeclarationRef { @@ -59,9 +21,7 @@ data cli_run_floor_lens_observation_hand_rust_scaffold: Disposition = Scaffold { } } -data cli_run_floor_lens_hand_rust_dissolve_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: inert_lens_modules + lens_justification_census + refuse_on_module_graph_read_refusals + import_resolution_facts_with_observation — the 6A repoint's PRODUCTION census walk, justification census, typed read-refusal arm, and observation projection in HAND-Rust (counted interim seed growth, net +22 production LOC at landing; the host realization of the v2.lens.module_graph selection-tier reach until the census emits from workflow dag). DISSOLVES WHEN cli_run.rs Chunk F lands (docs/plans/cli-run-reconcile-defork.md — the census emits from workflow dag over v2.lens.module_graph and the HAND arms delete) OR ROADMAP 5-dissolve-patches (gunbc.roadmap_authority ticket) retires the HAND census entirely") - -data cli_run_floor_lens_hand_rust_loc_delta_net: Int = 22 +data cli_run_floor_lens_hand_rust_dissolve_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: refuse_on_module_graph_read_refusals + import_resolution_facts_with_observation — the typed read-refusal arm and the observation projection in HAND-Rust (the host realization of the v2.lens.module_graph fact production until it emits from workflow dag). The census walk and justification census this carrier also tracked are DELETED, not dissolved: the supply-side lens enforcement they served made every floor discovery run acquire a whole-corpus world to answer a question about lens authorship, and the answer had no consumer that justified the acquisition. DISSOLVES WHEN cli_run.rs Chunk F lands (docs/plans/cli-run-reconcile-defork.md) OR ROADMAP 5-dissolve-patches (gunbc.roadmap_authority ticket) retires the HAND fact production entirely") data cli_run_floor_lens_scaffold_shape_red_control: Disposition = Terminal { reason: "RED CONTROL for the scaffold-shape cells in dag/test/claim/cli_run_floor_lens_oracle_witness_test.dag: a Terminal disposition, so the canonical reader v2.lens.disposition_redundancy.disposition_is_terminal must answer true for it while answering false for every Scaffold row above. Without this row the shape assertions could pass on a reader that answered false unconditionally; with it, the reader is proven to discriminate. Not a disposition ABOUT any declaration — it is test data declared beside the rows it controls." @@ -69,8 +29,4 @@ data cli_run_floor_lens_scaffold_shape_red_control: Disposition = Terminal { data cli_run_floor_lens_oracle_receipt_plan_anchor: String = "docs/plans/cli-run-reconcile-defork.md" -data cli_run_floor_lens_oracle_equality_receipt_test: String = "facts_walk_matches_legacy_floor_lens_graph_on_live_corpus" - -data cli_run_floor_lens_oracle_build_count_receipt_test: String = "lens_census_single_facts_build_receipt" - -data cli_run_floor_lens_oracle_read_refusal_receipt_test: String = "unreadable_lens_is_a_read_refusal_not_an_absence" +data cli_run_floor_lens_oracle_read_refusal_receipt_test: String = "unreadable_source_is_a_read_refusal_not_an_absence" diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag index 52f7591be90..bdce88509ec 100644 --- a/dag/gunbc/design_document.dag +++ b/dag/gunbc/design_document.dag @@ -146,7 +146,7 @@ fn section_6_blocks() -> List { li(text: "**Model:** DFS the concept DAG before inventing vocabulary; fact-bundle modeling (invent or reuse on proven coincidence, never bare-alias); a finished stage is one fold (any non-fold residue is either a named irreducible kernel or un-migrated modeling — there is no third); model just-in-time and let the mark on the carrier be the authority (no parallel-ledger docs); **no scaffold lands by author declaration alone** — every net-new scaffold is represented by one exact dissolution obligation, joined to an external operator verdict on the current head, and refused in its absence (§5); reviewers independently search for undeclared scaffolds, so the author's classification is evidence to inspect, never the denominator."), li(text: "**Intellectual sustainability:** don't spend future author, reviewer, operator or maintainer time to buy present convenience. Work expected to be thrown away is *presumed redundant* (§2), so back up and complete the construction that will survive; use a temporary one only after the operator explicitly chooses that future cost. The reviewer's independent test, applied whether or not the author labelled anything: **will this artifact survive the terminal architecture substantially unchanged, and be consumed by it?** If no, presume scaffold and stop the merge until the final construction lands or the operator approves the exact exception. A *missing* dissolution condition makes the finding **more** severe, not less — the response is to name the undeclared dissolvable concept, request the final architecture, and require the exact obligation model if the author believes an exception is warranted; adding a trigger after review does not resolve the objection, it only makes the proposal eligible for a decision. Automated detection can never be the whole policy, because temporary work can be authored without using any of the names a gate matches on. Tells, each carrying a presumption: a hand-authored workflow, deployment script, migration script or operational command (out-of-band actuation); a second path beside an existing modeled route (parallel authority); \"bridge\", \"shim\", \"compatibility\", \"for now\", \"temporary\", \"until\", \"later\" (deferred refactor); a model to be deleted whole when the real one lands (throwaway model); a hand-authored projection the model should generate (manual application committed as source); raw shell implementing semantics already expressible in `.dag` (unmodeled realization); a broad wrapper around a type or modeling deficit (workaround hiding substrate work); a condition whose terminal is \"rewrite this properly\" (the proper work was not done); a new artifact with no final consumer (experimental residue). If dissolution approvals become frequent, that is not a process cost to optimize away — it is evidence the repository is routinely borrowing future intellectual labor to ship present convenience."), li(text: "**Prioritize holistically, not by the bottleneck:** balance the quantitative and the qualitative — don't anchor on one KPI (you'll hit it at a cost) or on pure taste. Map the cause→effect across sections; a 5ms step doesn't get a pass for not being the 80s one (it might be a 5ns step). One consequence is a standing rule, **bare minimum cost** (operator ruling 2026-07-10): a proven cost-shape defect — a copied accumulator, a quadratic fold — is *always fixed*, regardless of the realized n. \"n is small here\" is not a time-stable fact (§1/A3 — reuse changes n), and pricing per-site exceptions is itself redundant work (§2); the humility is not trusting your own \"negligible here.\" Root-cause to the language layer and fix related systems *together* — a local subsystem patch is the forked-logic trap. **Denominate the benefit:** the deliverable is a *displaced cost* (§1's time — a pain someone pays to remove); the lens/substrate is the *mechanism* (the moat), not the product. A lens — or any construction wall — is on-dial exactly insofar as it is the cheapest path to such a pain. Priced in elegance instead, the work is self-referential and unbounded (the purity trap — the economic twin of \"never\" in §5; an extensible substrate's infinite improvability dissolving its own bound)."), - li(text: "**Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie, so an **executable** hygiene check must keep every lens either wired (a discovered fail-closed witness) or deleted — that backstop runs over the corpus and is *not* superseded by the authoring-time construction-justification judgment, which layers on top of it."), + li(text: "**Enforce with lenses,** not grep — but **construction first** (§5): a lens is *validation* (it concedes the bad state is writable), so make the class unwritable by single authority where you can and reserve the lens for the unstructurable residue. As a residue mechanism it earns its keep: a pure reader over the same `Node` tree, storing nothing, so a new analysis costs zero substrate edits. Beware the tier where the machinery exists but nothing gates on it — coverage by illusion; an inert lens is itself a lie. **The corpus-wide backstops that used to police this are DELETED (2026-08-11), and the reason is the rule that replaces them:** the inert-lens reach census and the construction-justification census both ran inside floor witness discovery, so *every* discovery run — on every PR, on regen, in every coordinated worker — had to acquire a whole-corpus module graph in order to answer a question about who authored a lens. That is the §6 cost-shape defect at its purest: the unit of computation was the world, the unit of fact was one module's authorship, and the price was paid by every consumer that wanted a witness roster and nothing else. **Who paid it, split by era, because this document must not assert a superseded population as the present one:** before #8140 the walk was unconditional, so ordinary CI, regen, the falsifier cadence and every coordinated worker all paid; #8140 made it demand-directed, so a discovery-free plan such as regen stopped paying; from #8140 to this deletion the two censuses burdened every remaining discovery-bearing execution. The correction is recorded rather than reworded because a change deleting stale supply-side enforcement must not land a fresh stale assertion in the same diff (review on #8141). Neither census had a consumer that justified the acquisition; the inert-lens half additionally reported through two host builtins whose `.dag` surface was a pair of self-recursive stubs (`fn f() { f() }`) reachable only because the interpreter intercepted them. **What is NOT claimed:** this is a real scope narrowing, not a climb. A newly authored lens with no witness, and a lens recording no `construction_justification`, are both writable again and nothing detects either. The obligation survives as review diligence, which is strictly weaker. **Next-rung trigger:** an authorship fact belongs on the module's own declaration, checked at ingestion where the module is parsed anyway — one module's facts from one module's source — rather than reconstructed corpus-wide by a consumer that wanted something else. Until that lands the class sits at *mitigatable*, declared here rather than left to be rediscovered."), li(text: "*e.g.* one catamorphism `fold_node` is reused by all 7 v2 stages; #4699 dissolved `06_translate` 4,912→3,973 lines (`_go` accumulators 35→0); a 6-line `merge_envs` root fix cut reconcile from 81% of the pipeline to 6% (~2× self-compile) — the symptom recurs wherever the root is unfixed (v2 still hand-rolls `ParseTable` because the Realization carrier is staged, not inhabited)."), ]), ] diff --git a/dag/gunbc/plans/axiom_syllogism_lens.dag b/dag/gunbc/plans/axiom_syllogism_lens.dag index 27ac43ea068..2abbd16e557 100644 --- a/dag/gunbc/plans/axiom_syllogism_lens.dag +++ b/dag/gunbc/plans/axiom_syllogism_lens.dag @@ -113,7 +113,7 @@ fn axiom_syllogism_lens_body() -> List { rows: [ row(cells: [cell(text: "acyclicity / cycle detection"), cell(text: "`graph_has_multi_node_scc`"), cell(text: "`std/graph.dag`")]), row(cells: [cell(text: "forward/reverse adjacency, DFS"), cell(text: "`forward_adjacency` · `reverse_adjacency` · `dfs_finish_order`"), cell(text: "`std/graph.dag`")]), - row(cells: [cell(text: "reachability `universe ∖ reachable(roots)`"), cell(text: "the inert-lens / doc-graph BFS shape"), cell(text: "`inert_lens_modules` (`cli_run.rs`) · `doc_reachability_project.rs`")]), + row(cells: [cell(text: "reachability `universe ∖ reachable(roots)`"), cell(text: "the inert-lens / doc-graph BFS shape"), cell(text: "`doc_reachability_project.rs` (was also `inert_lens_modules`, DELETED gunbc#8141)")]), row(cells: [cell(text: "truth-value / syllogistic structure"), cell(text: "`Classical = True \\| False`"), cell(text: "`std/logic.dag`")]), row(cells: [cell(text: "well-founded / acyclic grounding"), cell(text: "initial-algebra + size-change"), cell(text: "`std/induction.dag`")]), row(cells: [cell(text: "fail-closed lens verdict carrier"), cell(text: "`LensVerdict` (Holds/Violation/NotApplicable/Unrealized)"), cell(text: "`std/lens_verdict.dag`")]), diff --git a/dag/gunbc/plans/construction_justification_rule.dag b/dag/gunbc/plans/construction_justification_rule.dag index d36b2124081..b20acf290fb 100644 --- a/dag/gunbc/plans/construction_justification_rule.dag +++ b/dag/gunbc/plans/construction_justification_rule.dag @@ -7,7 +7,7 @@ import gunbc.plans.md_helpers { h2, p, li, ul, cell, row } fn construction_justification_rule_body() -> List { [ - BlockquoteBlock { blocks: [p(text: "ROADMAP §0 meta-item. The authoring-time judgment that layers **on top of** the executable #5433 inert-lens backstop. DESIGN refs: §5 (construction over validation; the decidability trichotomy; the \"never\" trap), §6 (\"construction first\"; lenses are the residue mechanism; coverage-by-illusion), §7 (the recursion — make the lens discipline itself fail-closed). Sibling frame: [expressibility-frontier.md](expressibility-frontier.md) (the same three regions, generalized).")] }, + BlockquoteBlock { blocks: [p(text: "**SUPERSEDED IN PART — READ §5 BEFORE §2-§4 (2026-08-11, gunbc#8141).** Both executable halves this plan describes are DELETED: the #5433 inert-lens backstop and the fail-closed construction-justification presence check. Sections 2, 3 and 4 below are retained as the record of what was built and why, NOT as a description of the live floor — nothing in `discover_floor_corpus_rows` blocks an unreached or unjustified lens today. ROADMAP §0 meta-item. The authoring-time judgment that layered **on top of** the (now deleted) executable #5433 inert-lens backstop. DESIGN refs: §5 (construction over validation; the decidability trichotomy; the \"never\" trap), §6 (\"construction first\"; lenses are the residue mechanism; coverage-by-illusion), §7 (the recursion — make the lens discipline itself fail-closed). Sibling frame: [expressibility-frontier.md](expressibility-frontier.md) (the same three regions, generalized).")] }, h2(text: "1. The rule"), p(text: "DESIGN §6: a lens is **validation** — it concedes the bad state is *writable*. So **before adding any lens**, justify why its target bad-state class cannot be made *unwritable by construction* (single authority / realization derived from model). Convert what can be converted; reserve a lens only for the genuinely **unstructurable residue**. Each lens must classify its target class into one of DESIGN §5's three buckets:"), TableBlock { @@ -20,8 +20,8 @@ fn construction_justification_rule_body() -> List { ], }, p(text: "This is **not a parallel taxonomy** (§3): the names are DESIGN §5's, which [expressibility-frontier.md](expressibility-frontier.md) §2 generalizes into regions ①/②/③. The single authority for the typed model is `v2.lens.common.construction_justification`."), - h2(text: "2. Why this layers on the #5433 backstop — and does not supersede it"), - p(text: "The two checks cover the same set (`is_top_level_lens_module`) but answer different questions, and both run in `discover_floor_corpus_rows` (the seed floor-discovery walk, not new cemented Rust):"), + h2(text: "2. Why this layered on the #5433 backstop — and did not supersede it (HISTORICAL)"), + p(text: "The two checks covered the same set (`is_top_level_lens_module`) but answered different questions, and both ran in `discover_floor_corpus_rows` (the seed floor-discovery walk). Both are deleted as of gunbc#8141 — see §5:"), ul(items: [ li(text: "**#5433 inert-lens backstop** — *is this lens wired?* Every `v2.lens.*` module must be reached by a discovered fail-closed witness, or be deleted. Runs over the **corpus**; it is the floor guarantee."), li(text: "**construction-justification rule** (this) — *should this be a lens at all, and if so why?* Every `v2.lens.*` module must **record** its construction-justification."), @@ -31,17 +31,22 @@ fn construction_justification_rule_body() -> List { p(text: "The **judgment** (which class) is human and unstructurable — its *correctness* cannot be machine-verified (deciding decidability is itself ③, see frontier §6). But the **requirement to have recorded a judgment is structurable**, so we make the *missing-justification* state unwritable:"), ul(items: [ li(text: "**Carrier (the mark, §3/§6):** every lens module declares `data construction_justification: ConstructionJustification = …` — the judgment lives **on the lens**, not in a parallel ledger. This mirrors the `extdeps_external_authority_anchor` precedent (a fixed-name required decl per module)."), - li(text: "**Fail-closed presence check:** `discover_floor_corpus_rows` captures which lenses carry the decl during its single walk (zero extra IO) and **fails the floor closed** on any top-level lens that does not. A lens stripped of its justification goes **RED** (green-by-execution; discriminating on revert — `construction_justification_hygiene_tests`)."), + li(text: "**Fail-closed presence check (DELETED 2026-08-11, see §5):** `discover_floor_corpus_rows` captured which lenses carry the decl during its single walk and **failed the floor closed** on any top-level lens that did not. A lens stripped of its justification goes **RED** (green-by-execution; discriminating on revert — `construction_justification_hygiene_tests`)."), ]), p(text: "So the bad state (\"a lens with no recorded reason to be a lens\") is unwritable by construction, while the honest residue (is the recorded reason *true*?) stays review — exactly the partition the rule itself prescribes."), h2(text: "4. Status"), ul(items: [ li(text: "`v2.lens.common.construction_justification` — the typed model (`ConstructionClass` + `ConstructionJustification`)."), li(text: "All 35 top-level `v2.lens.*` modules carry a recorded justification (retroactive classification from each lens's existing header — the audit that surfaces any lens that is secretly a `WallNow`)."), - li(text: "Presence check + discriminating tests wired into `discover_floor_corpus_rows`."), + li(text: "~~Presence check + discriminating tests wired into `discover_floor_corpus_rows`~~ — **DELETED 2026-08-11 (gunbc#8141), see §5.**"), li(text: "**Vacuity residual — CLOSED.** Every `ConstructionClass` payload is now typed/grounded, no free string survives: the per-justification `rationale` and `RatchetForever`'s `undecidable_because` were removed (unverifiable §6 parallel-ledger prose no consumer reads); `WallAfterGrounding` carries the structured `dissolves_to: ConstructionMechanism`; and `WallNow`'s former free-text `construction` is now `{ mechanism: ConstructionMechanism, authority: DeclarationRef }` — the authority being the *one* `std.decl_ref.DeclarationRef` the disposition/determinism scaffold markers also bind through (no parallel ref type). So 'this lens chains to a real construction' is no longer prose but a **walkable graph property**: a host-side graph-property witness (`wall_now_authority_graph_is_total`) proves every `WallNow` authority resolves to a real top-level decl and goes RED on a planted dangling binding. That witness is a §6 scaffold (host-side resolution) dissolving onto a unified kind-agnostic decl-resolution primitive once exposed to `.dag`."), li(text: "**Residue / follow-on (honest):** the *correctness* of each recorded class is review, not gated. Modules recorded as `WallNow` (cost, application_serializer) and the support module `affected_set_examples` flag a §3 home question — they are computations/support filed under `v2.lens.*`, not validation lenses; relocating them is out of scope here (it touches module resolution) and is left as a marked follow-up."), ]), + h2(text: "5. Enforcement deleted (2026-08-11, gunbc#8141)"), + p(text: "Both executable checks described above ran inside floor witness discovery, and both answered a question about who authored a lens by acquiring a **whole-corpus module graph**. Every discovery run paid that acquisition. Split by era, since the population changed underneath this plan: before gunbc#8140 the roster walk was unconditional, so ordinary CI, regen, the falsifier cadence and every coordinated worker all paid; #8140 made it demand-directed and regen stopped paying; from there to gunbc#8141 the two censuses burdened every remaining discovery-bearing execution — all of which wanted a witness roster and nothing else. That is the DESIGN §6 cost-shape defect in its clearest form: the unit of computation was the world, the unit of fact was one module's authorship, and no consumer of either census justified the price. The inert-lens half additionally reported through two host builtins whose entire `.dag` surface was a pair of self-recursive stubs reachable only because the interpreter intercepted the spelling."), + p(text: "**What that costs, stated as a regression rather than implied.** A newly authored lens with no discovered witness, and a lens recording no `construction_justification`, are both writable again and **nothing detects either**. The 35-module population §4 reports as fully classified is a historical measurement, not a maintained invariant — a lens added tomorrow with no justification lands green. The obligation survives only as review diligence, which is strictly weaker than the check it replaces, and this plan is not evidence that it holds."), + p(text: "**Next-rung trigger.** An authorship fact belongs on the module's own declaration, checked at ingestion where that module is already parsed — one module's facts derived from one module's source — rather than reconstructed corpus-wide by a consumer that wanted something else. The `data construction_justification` carrier §3 describes is already the right shape for that; what was wrong was where the check ran, not where the fact lives. Until that lands the class sits at *mitigatable* under DESIGN §4b, declared here so it stays rankable."), + p(text: "What survived the deletion: `v2.lens.common.construction_justification` (the typed model), every lens module's recorded `construction_justification` decl, and `wall_now_authority_graph_is_total` — the WallNow authority-resolution witness, which is a separate graph property and still executes."), ] } @@ -49,6 +54,6 @@ data construction_justification_rule_plan: Plan = Plan { slug: "construction-justification-rule", title: "The construction-justification rule (authoring-time) — §0", body: construction_justification_rule_body(), - retirement: PlanRetiresWhen { condition: unbound_dissolution(description: "Delete this doc when the construction-justification rule is fully built: v2.lens.common.construction_justification is the single-authority typed model, every top-level v2.lens.* module carries a recorded justification, and the fail-closed presence check plus discriminating tests run in discover_floor_corpus_rows — at which point the rule is a witnessed property of the floor (the vacuity residual and the per-class correctness review being the honest §3-buckets that remain) and this design doc is redundant.") + retirement: PlanRetiresWhen { condition: unbound_dissolution(description: "SUPERSEDED TRIGGER (2026-08-11, gunbc#8141): the original condition named the fail-closed presence check running in discover_floor_corpus_rows, and that check is deleted, so the trigger as written can never fire — an unreachable condition is a lifecycle claim that structurally cannot report itself satisfied. Replacement: delete this doc when the construction-justification requirement is re-established at ingestion — the authorship fact checked where the module is already parsed, one module's facts from one module's source, rather than reconstructed corpus-wide by a consumer that wanted a witness roster — at which point the rule is again a witnessed property and this design doc is redundant. Until then the doc is retained as the record of what was built, why it was deleted, and what the repository currently does NOT enforce.") } } diff --git a/dag/gunbc/plans/inert_layer_lens.dag b/dag/gunbc/plans/inert_layer_lens.dag index 5924b78107a..93337db475e 100644 --- a/dag/gunbc/plans/inert_layer_lens.dag +++ b/dag/gunbc/plans/inert_layer_lens.dag @@ -68,13 +68,13 @@ fn inert_layer_lens_body() -> List { }, p(text: "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."), h2(text: "3. Two tiers (what's buildable now vs gated)"), - p(text: "**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."), + p(text: "**Tier 1 — module-level. SUPERSEDED SOURCE (2026-08-11, gunbc#8141): do NOT reuse #5433 — it no longer exists.** `inert_lens_modules` and the whole #5433 floor backstop were DELETED, because that census answered a lens-authorship question by acquiring a whole-corpus module graph inside every floor discovery. Its surviving replacement as the reachability authority is `v2.lens.module_graph` (selection-tier import + reference edges), whose live consumer is affected-set selection; `doc_reachability_project.rs` is the same BFS shape over doc nodes. The paragraph below is retained as the historical design, with its subject repointed: what it describes as \"reuse the existing walk\" now means \"build the walk over the module-graph facts\", which is a larger job than it reads. Historically, `inert_lens_modules` computed module-import transitive closure from seed roots and reported 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."), p(text: "**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."), h2(text: "4. The load-bearing ranking (the advisory half)"), p(text: "\"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."), h2(text: "5. Frontier placement (per [expressibility-frontier](expressibility-frontier.md))"), ul(items: [ - li(text: "**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."), + li(text: "**Inertness is a ① wall candidate.** Reachability is decidable; an inert load-bearing carrier should eventually **fail closed** as #5433 once did for lenses (\"an inert lens is a lie\" → \"an inert load-bearing carrier is a lie\") — stated in the past tense because that backstop is deleted (gunbc#8141) and no lens-inertness gate runs today. 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."), li(text: "**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)."), li(text: "**The ranking is the ② residue**, permanently advisory (judging \"load-bearing\" needs domain knowledge)."), ]), @@ -83,7 +83,7 @@ fn inert_layer_lens_body() -> List { header: row(cells: [cell(text: "need"), cell(text: "reuse"), cell(text: "file")]), alignments: [AlignNone, AlignNone, AlignNone], rows: [ - row(cells: [cell(text: "transitive reachability BFS"), cell(text: "`inert_lens_modules`"), cell(text: "`cli_run.rs:2558-2606`")]), + row(cells: [cell(text: "transitive reachability BFS"), cell(text: "`v2.lens.module_graph` selection-tier edges (was `inert_lens_modules`, DELETED gunbc#8141)"), cell(text: "`module_graph.dag` + `cli_run.rs` `build_module_graph_facts_live`")]), row(cells: [cell(text: "enumerate all declared concepts"), cell(text: "`concept_index.enumerate_concepts()`"), cell(text: "`concept_index.dag:130`")]), row(cells: [cell(text: "use vs structural edge classification"), cell(text: "`unused_parameters` `UseRelation` (`BindsTo` = the use authority)"), cell(text: "`unused_parameters.dag:22`")]), row(cells: [cell(text: "import/reference edge-walk"), cell(text: "`v2.std.layer` `LayerImportFact` projection"), cell(text: "`layer.dag` + `cli_run.rs:layer_import_facts`")]), @@ -94,7 +94,7 @@ fn inert_layer_lens_body() -> List { ul(items: [ li(text: "Tier 1 lands as `v2.lens.inert_layer` + a floor witness; runs over the corpus, **reports** (advisory) first, ranked, with the exception roster."), li(text: "Promote to fail-closed once the roster is small and stable (per §5 above)."), - li(text: "**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."), + li(text: "**Load-bearing seed caveat:** Tier 1 touches `cli_run.rs` — a DESIGN-named load-bearing file → **escalate before editing**. The former advice here was to extend `inert_lens_modules` behind a flag rather than fork it; that function is DELETED (gunbc#8141) and there is nothing to extend. Whatever Tier 1 becomes, it must not reintroduce a corpus-wide walk inside floor discovery — that placement, not the walk, is what the deletion removed."), li(text: "**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."), ]), h2(text: "8. Generalization — one rule, N substrates (code · docs · lenses)"), @@ -118,7 +118,7 @@ fn inert_layer_lens_body() -> List { li(text: "**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)."), ]), p(text: "**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.)"), - p(text: "**LANDED — the doc-graph wall is live (gunbc#5484), with one premise correction.** The \"no host bridges\" claim above holds **only for the dangling half**. The *orphan* half is `universe ∖ reachable`, and the universe is `docs/**/*.md` — which requires filesystem **enumeration**, and there is no list-dir host effect in `.dag` today (`std/filesystem` exposes only `Read`/`Write`). So the orphan half is host-fed: `src/v1/stage0/src/doc_reachability_project.rs` walks the tree and exposes two scalar verdicts (`doc_graph_orphan_count` / `doc_graph_dangling_link_count`) through the same additive corpus-gate builtin seam as `extdeps_external_authority_live_clean_tree_holds` / `fact_cardinality_*` (it does **not** touch `cli_run.rs`'s #5433 closure). The reachability primitive is the **same BFS shape** as `inert_lens_modules` re-expressed over doc nodes — the §3-single-authority doc *instance* of the one rule, not a forked concept. The dangling half alone *is* expressible in pure `.dag` (`filesystem_read` BFS from roots). **DISSOLUTION TRIGGER:** when `.dag` gains list-dir / compile-graph access (gunbc#5364, the Tier-2 note), the dir-walk + BFS fold into a pure `.dag` reader and the Rust census deletes. Re-derived against the **live** tree at landing: **22 docs, 22 reachable, 0 orphans, 0 dangling** — clean, because this PR added the five missing inbound links + a `docs/runbooks/README.md` index root (the runbook-kind root) and linked the runbook from it. Witness: `dag/test/claim/doc_reachability_witness_test.dag` (floor-discovered `test fn`s, fail-closed, RED on revert); RED/GREEN controls over a synthetic graph in the project module's unit tests."), + p(text: "**LANDED — the doc-graph wall is live (gunbc#5484), with one premise correction.** The \"no host bridges\" claim above holds **only for the dangling half**. The *orphan* half is `universe ∖ reachable`, and the universe is `docs/**/*.md` — which requires filesystem **enumeration**, and there is no list-dir host effect in `.dag` today (`std/filesystem` exposes only `Read`/`Write`). So the orphan half is host-fed: `src/v1/stage0/src/doc_reachability_project.rs` walks the tree and exposes two scalar verdicts (`doc_graph_orphan_count` / `doc_graph_dangling_link_count`) through the same additive corpus-gate builtin seam as `extdeps_external_authority_live_clean_tree_holds` / `fact_cardinality_*` (it does **not** touch `cli_run.rs`'s #5433 closure). The reachability primitive is the **same BFS shape** as the then-live `inert_lens_modules` (DELETED gunbc#8141) re-expressed over doc nodes — the §3-single-authority doc *instance* of the one rule, not a forked concept. The dangling half alone *is* expressible in pure `.dag` (`filesystem_read` BFS from roots). **DISSOLUTION TRIGGER:** when `.dag` gains list-dir / compile-graph access (gunbc#5364, the Tier-2 note), the dir-walk + BFS fold into a pure `.dag` reader and the Rust census deletes. Re-derived against the **live** tree at landing: **22 docs, 22 reachable, 0 orphans, 0 dangling** — clean, because this PR added the five missing inbound links + a `docs/runbooks/README.md` index root (the runbook-kind root) and linked the runbook from it. Witness: `dag/test/claim/doc_reachability_witness_test.dag` (floor-discovered `test fn`s, fail-closed, RED on revert); RED/GREEN controls over a synthetic graph in the project module's unit tests."), h2(text: "9. Open"), ul(items: [ li(text: "**LANDED — the code symbol-level inert-CARRIER instance (Lane 7, this PR).** `v2.lens.inert_carrier` over `src/v1/stage0/src/inert_carrier_project.rs` flags a *type carrier* that is **defined + self-tested + zero real consumer** (DESIGN §5 coverage-by-illusion). The landing took the **coverage-by-illusion** reading of §1 rather than run-root reachability: a carrier is inert iff it is self-tested (named in a `*_test.dag`) AND used by zero non-test code outside its own declaration block. The `self-tested` gate is the key — it filters from \"every staged-ahead carrier\" (the model-first discipline this whole doc defends) down to the precise §5 trap (a green test, no production consumer), yielding a small, high-confidence set (8 carriers: AccessPolicy, CargoDependency, CargoPackage, FilePermissions, FloorWitnessRow, GitCliReportedVersion, ReactHookSite, SecretValue) rather than the hundreds a raw reachability sweep returns. (Seeded at 9; `RbacPolicy` then dissolved off the roster the moment a real consumer landed — `extdeps/bmc/access.dag`'s `redfish_rbac_policy` — exactly the stale-roster ratchet doing its job.) Fail-closed floor witness (`src/v2/lens/inert_carrier_test.dag`), named shrinking roster + stale-roster ratchet, discriminating synthetic RED/GREEN host controls. This is the Tier-2-host-fed path of §3 (not the cli_run.rs Tier-1 closure); DISSOLUTION at gunbc#5364. The run-root-reachability variant below (CacheLayerPlan/WorkDemand — NOT self-tested, so out of this instance's scope) remains the next, distinct cut."), diff --git a/dag/gunbc/roadmap_authority.dag b/dag/gunbc/roadmap_authority.dag index be0b4cca3eb..7c8fecae583 100644 --- a/dag/gunbc/roadmap_authority.dag +++ b/dag/gunbc/roadmap_authority.dag @@ -2537,7 +2537,7 @@ data scm_prerequisite_acceptance_note: String = "The operator explicitly accepte data scm_p0_acceptance_evidence_note: String = "P0 acceptance maps the roadmap clauses through test.claim.source_integration_landing_spine_witness witness_p0_roadmap_acceptance_contract_holds: all seven removed closure receipts stay machine-owned; evidence support/challenge/neither/conflict and terminal blocking do not become a preference question; both material alternatives resume by structural position; authorization, self-amendment, exhausted-bound, and permanent-effect failures keep their typed internal refusal and plain terminal projection; stale-parent work retries internally; a committed independently read-back transition stays Landed through projection failure; the audience projection excludes internal theory and manual Git-repair vocabulary; and the successful path retains its ordinary Git compatibility receipt. The same aggregate executes the explicit 50-agent/10-overlap/30-minute stress profile and timestamp non-authority. Handback remains bounded exactly at P0: gunbc.source_integration_landing_spine names the absent P1 proof kernel, P2 capture/edit lens, and P3 effect transport; none is claimed or activated by this receipt." -data v1_interpreter_primitive_roster_acceptance_note: String = "ACCEPTED AT THE NARROWED BAR, WITH ONE HANDBACK CLAUSE GENUINELY AMENDED RATHER THAN REWORDED -- read the digest move as a real change to the bar, which is exactly the check criteria_digest_reword_note asks a reviewer to perform. The clause as #7558 landed it demanded 'witnesses asserting exact values rather than lower bounds'. Those witnesses no longer exist on main: #7615 deleted the five that pinned live-population counts (7 dispatch sites, 183 derived rows, 2 declared rows, 174 arm identities, 161 authored spellings) because DESIGN.md 5 rules that a measurement copied from the same current tree is not an oracle -- and those five had already behaved exactly as that rule predicts, as a change detector that redded main twice (#7575 landed one derived arm short, #7614 repaired, #7615 removed the class). Accepting against the original wording would have required either restoring a forbidden oracle or calling a clause satisfied that plainly was not.\n\nWHAT REPLACED IT IS STRONGER, WHICH IS WHY THIS IS NOT A LOWERED BAR. The deleted clause existed so that a silently dropped arm stays detectable, which a lower-bound witness cannot do. Every exact assertion grounded in a NAMED identity or a controlled fixture survived #7615 untouched: free_call_shadowing_is_exactly_the_two_inert_lens_bridges and method_call_shadowing_is_exactly_the_known_lookup_case assert exact shadow sets by member name; the_two_shadowed_arm_identities_under_lookup_are_exactly_the_expected_pair pins both identities; the_declared_residue_is_exactly_the_two_non_match_arm_sites is a two-directional set equality by name rather than a count. Only the tree-copied census literals went, which is precisely the line DESIGN.md 5 draws when it says the rule rejects tree-copied census pins while preserving exact-count fixture tests. The three denominators were NOT deleted: dispatch_site_count, distinct_arm_identity_count and authored_spelling_count all remain derived from the roster rather than pinned as literals, which is what this node's handback asks for. AN EARLIER DRAFT OF THIS NOTE OVERCLAIMED WHAT CONSUMES THEM, and the correction is recorded here rather than quietly edited because it is the same failure this repository keeps paying for -- a sentence that reads well while the evidence it cites does not establish it (caught in review 46995). That draft said all three 'gained a live consumer at D1' which 'joins census to roster by identity'. Neither half was true. What test.claim.primitive_identity_join_witness w_interpreter_census_consumes_roster_authority actually executes is distinct_arm_identity_count, authored_spelling_count and v1_interpreter_row_count: it asserts the ordering relation the deleted witness used to pin, plus primitive_d0_interpreter_census_matches_roster, which is primitive_d0_interpreter_surface_row_count() == v1_interpreter_row_count() -- a COUNT EQUALITY between two independent derivations of the same population, not an identity join. That is a legitimate cross-derivation reconciliation and it is not a tree-copied census literal, but DESIGN.md 5 is explicit that completeness is an identity join rather than a count equality, so it must not be described as one. And dispatch_site_count has NO external consumer at all: the only mention outside its own carrier is this note. That is named here as residue rather than counted as delivered. DISSOLVE-ON: the D0 identity join reaching arm grain, at which point the census and the roster reconcile by row identity and the count equality is replaced rather than supplemented.\n\nEVIDENCE, DERIVED BY EXECUTION. Digest 581758f45921b40a was produced by running node_criteria_digest against the live amended node on this tree, not transcribed or hand-computed; the discriminating control for the pin itself is that two earlier wordings of the same row yield different values -- d2e455ab49e472e2 before any amendment, f0f450f4ddc82fe9 before the review-46995 correction to the denominator clause -- so the stored digest demonstrably tracks the criteria text rather than merely existing, and each correction to the bar has been re-derived rather than carried forward. All 19 witnesses in test.claim.v1_interpreter_primitive_surface_witness_test executed green on a binary REBUILT AT THIS HEAD, which matters more here than in most acceptances: the roster derives from macro token lists compiled INTO the binary, so a stale target answers about a tree that no longer exists, and that is exactly how #7575's shortfall stayed invisible to local runs. The named red_control is shadow_detector_catches_a_planted_duplicate, the planted-defect RED discharging this row's second red_control arm, paired with shadow_detector_admits_a_real_alias_pair so that a detector refusing legitimate aliases would fail too.\n\nWHAT THIS RECEIPT DOES NOT CLAIM. The first red_control arm -- an arm without a row and a row without an arm are both unwritable -- is discharged BY CONSTRUCTION, one macro token list expanding both, and therefore has no executing witness by design; the node's own first_slice already states it is mechanically preventive for the sites it covers and explicitly not structural, because a whole new dispatch site can still be added in Rust unnoticed. Closing that is v1-interpreter-primitive-dispatch-authority, which is NOT implemented and NOT accepted here -- and the record needs one correction, because a rollup briefly read it as landed: PR #7624 carried the title 'Lane B: interpreter roster R1 -- invert dispatch authority from Rust to the .dag roster', but its entire merged diff is two lines adding `import std.types { NonEmptyStr }` to this carrier. It inverted no authority, generated no dispatch, and deleted no Rust-side denominator; it is a harmless missing-import repair whose title described work that was never written (operator correction, 2026-08-02). R1 is unstarted, so accepting R0 here advances the frontier to an unimplemented successor rather than past it. The third arm -- a roster able to represent an arm carrying no semantic primitive identity -- holds STRUCTURALLY, because InterpreterPrimitiveDispatchArm carries an interpreter-local arm identity and no semantic-primitive-identity field at all, so every row already is such an arm and the closing contract shows the roster's operations are total over one. An earlier cut of that clause discharged it with D1's primitive_d0_derived_rows_missing_identity_count() > 0, which measures how far the semantic identity join has got rather than what the roster can carry, and would have gone red exactly when the join succeeded for every derived row -- legitimate downstream progress reddening an upstream node's acceptance check, the same defect class #7615 removed from the census witnesses relocated onto join state (caught in review 46974, corrected before merge). The seed-file reconciliation clause is delivered as a construction plus a named residue (every primitive arm now carries the token form arm \"identity\" { \"spelling\" } =>, so the residue is whatever stays bare) and is NOT asserted by an executing witness; that is a real limit of this handback, stated rather than implied." +data v1_interpreter_primitive_roster_acceptance_note: String = "ACCEPTED AT THE NARROWED BAR, WITH ONE HANDBACK CLAUSE GENUINELY AMENDED RATHER THAN REWORDED -- read the digest move as a real change to the bar, which is exactly the check criteria_digest_reword_note asks a reviewer to perform. The clause as #7558 landed it demanded 'witnesses asserting exact values rather than lower bounds'. Those witnesses no longer exist on main: #7615 deleted the five that pinned live-population counts (7 dispatch sites, 183 derived rows, 2 declared rows, 174 arm identities, 161 authored spellings) because DESIGN.md 5 rules that a measurement copied from the same current tree is not an oracle -- and those five had already behaved exactly as that rule predicts, as a change detector that redded main twice (#7575 landed one derived arm short, #7614 repaired, #7615 removed the class). Accepting against the original wording would have required either restoring a forbidden oracle or calling a clause satisfied that plainly was not.\n\nWHAT REPLACED IT IS STRONGER, WHICH IS WHY THIS IS NOT A LOWERED BAR. The deleted clause existed so that a silently dropped arm stays detectable, which a lower-bound witness cannot do. Every exact assertion grounded in a NAMED identity or a controlled fixture survived #7615 untouched: free_call_shadowing_is_exactly_the_two_inert_lens_bridges and method_call_shadowing_is_exactly_the_known_lookup_case assert exact shadow sets by member name (CITATION CORRECTION, 2026-08-11: the first of those no longer exists under that name. The inert-lens census, its two host builtins and the v2.lens.inert_lens module were deleted whole, so the free-call shadow set emptied and the witness became free_call_carries_no_shadowed_spelling, an exact set assertion over an empty set rather than over two named members. That is a genuinely weaker witness than the one this note cites as surviving evidence -- an empty-set claim cannot discriminate a detector that never reports -- and the discrimination is carried instead by the planted-duplicate controls and by method_call_shadowing_is_exactly_the_known_lookup_case, which still pins a named member. Recorded here rather than silently reworded, because the sentence was cited as evidence and the evidence changed); the_two_shadowed_arm_identities_under_lookup_are_exactly_the_expected_pair pins both identities; the_declared_residue_is_exactly_the_two_non_match_arm_sites is a two-directional set equality by name rather than a count. Only the tree-copied census literals went, which is precisely the line DESIGN.md 5 draws when it says the rule rejects tree-copied census pins while preserving exact-count fixture tests. The three denominators were NOT deleted: dispatch_site_count, distinct_arm_identity_count and authored_spelling_count all remain derived from the roster rather than pinned as literals, which is what this node's handback asks for. AN EARLIER DRAFT OF THIS NOTE OVERCLAIMED WHAT CONSUMES THEM, and the correction is recorded here rather than quietly edited because it is the same failure this repository keeps paying for -- a sentence that reads well while the evidence it cites does not establish it (caught in review 46995). That draft said all three 'gained a live consumer at D1' which 'joins census to roster by identity'. Neither half was true. What test.claim.primitive_identity_join_witness w_interpreter_census_consumes_roster_authority actually executes is distinct_arm_identity_count, authored_spelling_count and v1_interpreter_row_count: it asserts the ordering relation the deleted witness used to pin, plus primitive_d0_interpreter_census_matches_roster, which is primitive_d0_interpreter_surface_row_count() == v1_interpreter_row_count() -- a COUNT EQUALITY between two independent derivations of the same population, not an identity join. That is a legitimate cross-derivation reconciliation and it is not a tree-copied census literal, but DESIGN.md 5 is explicit that completeness is an identity join rather than a count equality, so it must not be described as one. And dispatch_site_count has NO external consumer at all: the only mention outside its own carrier is this note. That is named here as residue rather than counted as delivered. DISSOLVE-ON: the D0 identity join reaching arm grain, at which point the census and the roster reconcile by row identity and the count equality is replaced rather than supplemented.\n\nEVIDENCE, DERIVED BY EXECUTION. Digest 581758f45921b40a was produced by running node_criteria_digest against the live amended node on this tree, not transcribed or hand-computed; the discriminating control for the pin itself is that two earlier wordings of the same row yield different values -- d2e455ab49e472e2 before any amendment, f0f450f4ddc82fe9 before the review-46995 correction to the denominator clause -- so the stored digest demonstrably tracks the criteria text rather than merely existing, and each correction to the bar has been re-derived rather than carried forward. All 19 witnesses in test.claim.v1_interpreter_primitive_surface_witness_test executed green on a binary REBUILT AT THIS HEAD, which matters more here than in most acceptances: the roster derives from macro token lists compiled INTO the binary, so a stale target answers about a tree that no longer exists, and that is exactly how #7575's shortfall stayed invisible to local runs. The named red_control is shadow_detector_catches_a_planted_duplicate, the planted-defect RED discharging this row's second red_control arm, paired with shadow_detector_admits_a_real_alias_pair so that a detector refusing legitimate aliases would fail too.\n\nWHAT THIS RECEIPT DOES NOT CLAIM. The first red_control arm -- an arm without a row and a row without an arm are both unwritable -- is discharged BY CONSTRUCTION, one macro token list expanding both, and therefore has no executing witness by design; the node's own first_slice already states it is mechanically preventive for the sites it covers and explicitly not structural, because a whole new dispatch site can still be added in Rust unnoticed. Closing that is v1-interpreter-primitive-dispatch-authority, which is NOT implemented and NOT accepted here -- and the record needs one correction, because a rollup briefly read it as landed: PR #7624 carried the title 'Lane B: interpreter roster R1 -- invert dispatch authority from Rust to the .dag roster', but its entire merged diff is two lines adding `import std.types { NonEmptyStr }` to this carrier. It inverted no authority, generated no dispatch, and deleted no Rust-side denominator; it is a harmless missing-import repair whose title described work that was never written (operator correction, 2026-08-02). R1 is unstarted, so accepting R0 here advances the frontier to an unimplemented successor rather than past it. The third arm -- a roster able to represent an arm carrying no semantic primitive identity -- holds STRUCTURALLY, because InterpreterPrimitiveDispatchArm carries an interpreter-local arm identity and no semantic-primitive-identity field at all, so every row already is such an arm and the closing contract shows the roster's operations are total over one. An earlier cut of that clause discharged it with D1's primitive_d0_derived_rows_missing_identity_count() > 0, which measures how far the semantic identity join has got rather than what the roster can carry, and would have gone red exactly when the join succeeded for every derived row -- legitimate downstream progress reddening an upstream node's acceptance check, the same defect class #7615 removed from the census witnesses relocated onto join state (caught in review 46974, corrected before merge). The seed-file reconciliation clause is delivered as a construction plus a named residue (every primitive arm now carries the token form arm \"identity\" { \"spelling\" } =>, so the residue is whatever stays bare) and is NOT asserted by an executing witness; that is a real limit of this handback, stated rather than implied." type RoadmapAcceptanceReceiptsProjection = RoadmapAcceptanceReceiptsProjected { receipts: List } diff --git a/dag/gunbc/v1_interpreter_dispatch_emit.dag b/dag/gunbc/v1_interpreter_dispatch_emit.dag index da6f3da2ee6..185c134e5c3 100644 --- a/dag/gunbc/v1_interpreter_dispatch_emit.dag +++ b/dag/gunbc/v1_interpreter_dispatch_emit.dag @@ -59,7 +59,7 @@ fn arm_identity_to_rust_variant(identity: String) -> String { |> join(separator: "") } -data module_domain_prefix_note: String = "Every EvalCallBridgeFamilySite.module is REQUIRED to be dotted under the v2. namespace (v2.std.node, v2.lens.inert_lens, ...); module_domain_prefix_ok checks that structurally rather than assuming it from what the roster happens to contain today (operator correction, PR 7801, 2026-08-04 — the prior note recorded an observation about the live roster, not a requirement, so a later non-v2 bridge family would have silently lost its domain segment through an unconditional drop). module_pascal_after_domain_prefix/module_slug_after_domain_prefix drop that leading segment before naming the per-family generated enum/lookup/macro, mirroring arm_identity_to_rust_variant's own dot-segment PascalCase fold — one algorithm, read twice — but only after the domain segment is confirmed to be the one being dropped." +data module_domain_prefix_note: String = "Every EvalCallBridgeFamilySite.module is REQUIRED to be dotted under the v2. namespace (v2.std.node, v2.std.data_index, ...); module_domain_prefix_ok checks that structurally rather than assuming it from what the roster happens to contain today (operator correction, PR 7801, 2026-08-04 — the prior note recorded an observation about the live roster, not a requirement, so a later non-v2 bridge family would have silently lost its domain segment through an unconditional drop). module_pascal_after_domain_prefix/module_slug_after_domain_prefix drop that leading segment before naming the per-family generated enum/lookup/macro, mirroring arm_identity_to_rust_variant's own dot-segment PascalCase fold — one algorithm, read twice — but only after the domain segment is confirmed to be the one being dropped." fn expected_bridge_family_domain_segment() -> String { "v2" diff --git a/dag/gunbc/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1_interpreter_primitive_surface.dag index 228872a34e6..37bd67155ed 100644 --- a/dag/gunbc/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1_interpreter_primitive_surface.dag @@ -1246,24 +1246,6 @@ fn v1_interpreter_authored_roster_arms() -> List List List { "test_migration_delete_guard_uncovered_deletes", "inert_carrier_names_live", "inert_carrier_declared_count", - "inert_lens_unreached_module_count", - "inert_lens_top_level_module_count", "non_fold_residue_count", "non_fold_residue_unrostered_count", "non_fold_residue_stale_roster_count", diff --git a/dag/test/claim/cli_run_floor_lens_oracle_witness_test.dag b/dag/test/claim/cli_run_floor_lens_oracle_witness_test.dag index 3fc54aae302..b211ef6ad31 100644 --- a/dag/test/claim/cli_run_floor_lens_oracle_witness_test.dag +++ b/dag/test/claim/cli_run_floor_lens_oracle_witness_test.dag @@ -4,62 +4,25 @@ import std.dissolution { dissolution_description } import v2.lens.disposition_redundancy { disposition_is_terminal } import gunbc.cli_run_floor_lens_oracle_scaffold { - cli_run_floor_lens_legacy_graph_oracle_scaffold, - cli_run_floor_lens_legacy_walk_oracle_scaffold, - cli_run_floor_lens_census_walk_hand_rust_scaffold, - cli_run_floor_lens_justification_hand_rust_scaffold, cli_run_floor_lens_read_refusal_hand_rust_scaffold, cli_run_floor_lens_observation_hand_rust_scaffold, cli_run_floor_lens_scaffold_shape_red_control, - cli_run_floor_lens_oracle_dissolve_trigger, cli_run_floor_lens_hand_rust_dissolve_trigger, - cli_run_floor_lens_hand_rust_loc_delta_net, - cli_run_floor_lens_oracle_equality_receipt_test, - cli_run_floor_lens_oracle_build_count_receipt_test, cli_run_floor_lens_oracle_read_refusal_receipt_test, } -test fn floor_lens_legacy_graph_oracle_is_declared_scaffold() -> Bool { - !disposition_is_terminal(d: cli_run_floor_lens_legacy_graph_oracle_scaffold) -} - -test fn floor_lens_legacy_walk_oracle_is_declared_scaffold() -> Bool { - !disposition_is_terminal(d: cli_run_floor_lens_legacy_walk_oracle_scaffold) -} - test fn floor_lens_hand_rust_production_arms_are_declared_scaffolds() -> Bool { - !disposition_is_terminal(d: cli_run_floor_lens_census_walk_hand_rust_scaffold) && - !disposition_is_terminal(d: cli_run_floor_lens_justification_hand_rust_scaffold) && - !disposition_is_terminal(d: cli_run_floor_lens_read_refusal_hand_rust_scaffold) && + !disposition_is_terminal(d: cli_run_floor_lens_read_refusal_hand_rust_scaffold) && !disposition_is_terminal(d: cli_run_floor_lens_observation_hand_rust_scaffold) } test fn floor_lens_scaffold_shape_reader_discriminates() -> Bool { - !disposition_is_terminal(d: cli_run_floor_lens_census_walk_hand_rust_scaffold) + !disposition_is_terminal(d: cli_run_floor_lens_read_refusal_hand_rust_scaffold) && disposition_is_terminal(d: cli_run_floor_lens_scaffold_shape_red_control) } -test fn floor_lens_oracle_dissolve_trigger_names_sites_and_lane() -> Bool { - string_contains( - s: dissolution_description(condition: cli_run_floor_lens_oracle_dissolve_trigger), - pattern: "floor_lens_graph_legacy" - ) && - string_contains( - s: dissolution_description(condition: cli_run_floor_lens_oracle_dissolve_trigger), - pattern: "inert_lens_modules_legacy" - ) && - string_contains( - s: dissolution_description(condition: cli_run_floor_lens_oracle_dissolve_trigger), - pattern: "resolve_transitively_bfs_legacy" - ) && - string_contains( - s: dissolution_description(condition: cli_run_floor_lens_oracle_dissolve_trigger), - pattern: "cli-run-reconcile-defork" - ) -} - -test fn floor_lens_hand_rust_trigger_names_sites_ticket_and_loc() -> Bool { +test fn floor_lens_hand_rust_trigger_names_sites_and_ticket() -> Bool { string_contains( s: dissolution_description(condition: cli_run_floor_lens_hand_rust_dissolve_trigger), pattern: "refuse_on_module_graph_read_refusals" @@ -75,21 +38,12 @@ test fn floor_lens_hand_rust_trigger_names_sites_ticket_and_loc() -> Bool { string_contains( s: dissolution_description(condition: cli_run_floor_lens_hand_rust_dissolve_trigger), pattern: "cli-run-reconcile-defork" - ) && - cli_run_floor_lens_hand_rust_loc_delta_net > 0 + ) } -test fn floor_lens_oracle_executing_receipts_named() -> Bool { +test fn floor_lens_oracle_executing_receipt_named() -> Bool { string_contains( - s: cli_run_floor_lens_oracle_equality_receipt_test, - pattern: "matches_legacy_floor_lens_graph" - ) && - string_contains( - s: cli_run_floor_lens_oracle_build_count_receipt_test, - pattern: "single_facts_build" - ) && - string_contains( - s: cli_run_floor_lens_oracle_read_refusal_receipt_test, - pattern: "read_refusal_not_an_absence" - ) + s: cli_run_floor_lens_oracle_read_refusal_receipt_test, + pattern: "read_refusal_not_an_absence" + ) } diff --git a/dag/test/claim/long/inert_lens_hygiene_witness_test.dag b/dag/test/claim/long/inert_lens_hygiene_witness_test.dag deleted file mode 100644 index 8449ee8cee7..00000000000 --- a/dag/test/claim/long/inert_lens_hygiene_witness_test.dag +++ /dev/null @@ -1,12 +0,0 @@ -module test.claim.long.inert_lens_hygiene_witness - - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly - -test fn inert_lens_hygiene_has_no_unreached_modules() -> Bool { - return v2.lens.inert_lens.inert_lens_hygiene_has_no_unreached_modules_holds() -} - -test fn inert_lens_hygiene_universe_is_nonempty() -> Bool { - return v2.lens.inert_lens.inert_lens_hygiene_universe_is_nonempty_holds() -} diff --git a/dag/test/claim/v1_interpreter_primitive_dispatch_authority_acceptance_test.dag b/dag/test/claim/v1_interpreter_primitive_dispatch_authority_acceptance_test.dag index 1e50b09b8c9..df1251d7f98 100644 --- a/dag/test/claim/v1_interpreter_primitive_dispatch_authority_acceptance_test.dag +++ b/dag/test/claim/v1_interpreter_primitive_dispatch_authority_acceptance_test.dag @@ -1,7 +1,7 @@ module test.claim.v1_interpreter_primitive_dispatch_authority_acceptance import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } -import v2.std.qualified_name { qualified_name_from_dotted_string } +import v2.std.qualified_name { qualified_name_from_dotted_string, qualified_name_to_dotted_string } import gunbc.v1_interpreter_dispatch_emit { any_roster_site_has_rust_variant_collision, any_roster_site_has_spelling_collision, @@ -29,7 +29,7 @@ import gunbc.v1_interpreter_primitive_surface { data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data closing_contract_note: String = "THE CLOSING CHECK FOR v1-interpreter-primitive-dispatch-authority. R1 inverts the roster: gunbc.v1_interpreter_primitive_surface v1_interpreter_authored_roster_arms is the canonical authority; generated lookup in v1_interpreter_dispatch_generated.rs routes spellings to typed arm identities derived from arm identity, and the interpreter dispatch macros consult that lookup before matching handler bodies. The checks here are structural properties that survive roster growth -- not population pins.\n\nCOMPILE-TIME EXHAUSTIVENESS IS NOW UNIFORM ACROSS EVERY SITE. Every InterpreterPrimitiveDispatchArm names its own dispatch_emit_site, a closed InterpreterDispatchEmitSite field -- there is no prefix-convention parsing and no parallel hand-authored validator left to drift from it. eval_call_bridge is no longer one shared enum spanning nine v4 bridge families: each family (keyed by its own module, EvalCallBridgeFamilySite { module }) gets its own generated enum and lookup_* function, so a roster row added to one family without a matching handler body fails a non-exhaustive inner match on THAT family's generated enum at cargo build -- no unreachable! wildcard, no runtime degradation. eval_call_native_intercept was already single-family and already exhaustive; it only lost its dead per-arm spelling literal. VARIANT COLLISION refuses generation when two distinct arm identities within one emit site collapse to the same PascalCase enum name. SPELLING COLLISION refuses generation when two distinct arm identities within one emit site share one authored_spelling -- Rust's own unreachable-pattern lint is not a substitute for this refusal, and cross-site spelling reuse (lookup, dispatched both by the eval_method_call short-circuit and by the algebra arm it shadows) remains legal because the check is scoped per site. POSITIVE CONTROLS: dispatch_emit_succeeds_on_live_roster and src/v1/stage0/tests/interpreter_dispatch_authority.rs lookup coverage per site -- the latter calls each bridge family's own generated lookup_eval_call_bridge_ function by name (lookup_eval_call_bridge_std_node, lookup_eval_call_bridge_std_compilers_lexing) rather than one shared lookup_eval_call_bridge, and its distinctness assertions compare variants within one family's generated enum, never across two now-distinct enum types. DISCRIMINATING REDS ENROLLED HERE: bridge_family_sites_are_split_per_family_red_control, rust_variant_collision_synthetic_red_control, and spelling_collision_synthetic_red_control.\n\nWHAT MAKES THIS ABLE TO FAIL. Reintroducing a hand-authored per-arm spelling literal, collapsing the nine bridge families back onto one shared site key, dropping a declared residual row's dissolution trigger, removing the generated lookup path, or allowing variant- or spelling-colliding identities within one site each reds a clause. Reverting a row's provenance away from AuthoredInRoster or DeclaredHere is no longer even expressible: R1 closeout item SEVEN deleted the legacy DerivedFromDispatch variant from ArmEnumeration once the pre-R1 derivation model it marked was fully retired, so that invalid state climbed from a witness RED control to structurally impossible -- roster_rows_are_authored_in_roster_not_transcribed_from_rust and declared_residual_rows_retain_independent_dispositions below remain the exhaustive positive control over the two variants that do exist." +data closing_contract_note: String = "THE CLOSING CHECK FOR v1-interpreter-primitive-dispatch-authority. R1 inverts the roster: gunbc.v1_interpreter_primitive_surface v1_interpreter_authored_roster_arms is the canonical authority; generated lookup in v1_interpreter_dispatch_generated.rs routes spellings to typed arm identities derived from arm identity, and the interpreter dispatch macros consult that lookup before matching handler bodies. The checks here are structural properties that survive roster growth -- not population pins.\n\nCOMPILE-TIME EXHAUSTIVENESS IS NOW UNIFORM ACROSS EVERY SITE. Every InterpreterPrimitiveDispatchArm names its own dispatch_emit_site, a closed InterpreterDispatchEmitSite field -- there is no prefix-convention parsing and no parallel hand-authored validator left to drift from it. eval_call_bridge is no longer one shared enum spanning nine v4 bridge families: each family (keyed by its own module, EvalCallBridgeFamilySite { module }) gets its own generated enum and lookup_* function, so a roster row added to one family without a matching handler body fails a non-exhaustive inner match on THAT family's generated enum at cargo build -- no unreachable! wildcard, no runtime degradation. eval_call_native_intercept was already single-family and already exhaustive; it only lost its dead per-arm spelling literal. VARIANT COLLISION refuses generation when two distinct arm identities within one emit site collapse to the same PascalCase enum name. SPELLING COLLISION refuses generation when two distinct arm identities within one emit site share one authored_spelling -- Rust's own unreachable-pattern lint is not a substitute for this refusal, and cross-site spelling reuse (lookup, dispatched both by the eval_method_call short-circuit and by the algebra arm it shadows) remains legal because the check is scoped per site. POSITIVE CONTROLS: dispatch_emit_succeeds_on_live_roster and src/v1/stage0/tests/interpreter_dispatch_authority.rs lookup coverage per site -- the latter calls each bridge family's own generated lookup_eval_call_bridge_ function by name (lookup_eval_call_bridge_std_node, lookup_eval_call_bridge_std_compilers_lexing) rather than one shared lookup_eval_call_bridge, and its distinctness assertions compare variants within one family's generated enum, never across two now-distinct enum types. DISCRIMINATING REDS ENROLLED HERE: bridge_family_sites_are_split_per_family_red_control, rust_variant_collision_synthetic_red_control, and spelling_collision_synthetic_red_control. THAT FIRST CONTROL WAS A POPULATION PIN UNTIL 2026-08-11, contradicting this note's own opening claim that the checks here are structural properties rather than population pins: it asserted distinct_bridge_family_site_count() == 9, a literal copied from whatever the roster happened to contain. gunbc#8141 deleted the v2.lens.inert_lens bridge family and the pin redded on a population change rather than on a defect -- a change detector behaving exactly as DESIGN.md section 5 predicts, and the same class #7615 removed from the census witnesses. It is now DERIVED: the count of distinct emit-site keys must equal the count of distinct modules named by the bridge rows themselves, and that count must exceed one. This is not a tautology, because the two sides come from different places -- the left from dispatch_emit_site_key's keying, the right from each row's own module field -- so collapsing the families onto one shared key reds it (1 != N) while adding or removing a family does not. The clause now measures what its name claims and survives roster growth in both directions.\n\nWHAT MAKES THIS ABLE TO FAIL. Reintroducing a hand-authored per-arm spelling literal, collapsing the nine bridge families back onto one shared site key, dropping a declared residual row's dissolution trigger, removing the generated lookup path, or allowing variant- or spelling-colliding identities within one site each reds a clause. Reverting a row's provenance away from AuthoredInRoster or DeclaredHere is no longer even expressible: R1 closeout item SEVEN deleted the legacy DerivedFromDispatch variant from ArmEnumeration once the pre-R1 derivation model it marked was fully retired, so that invalid state climbed from a witness RED control to structurally impossible -- roster_rows_are_authored_in_roster_not_transcribed_from_rust and declared_residual_rows_retain_independent_dispositions below remain the exhaustive positive control over the two variants that do exist." fn roster_rows_are_authored_in_roster_not_transcribed_from_rust() -> Bool { count(v1_interpreter_authored_roster_arms()) > 0 @@ -75,10 +75,25 @@ fn distinct_bridge_family_site_count() -> Int { |> map(r => dispatch_emit_site_key(site: r.dispatch_emit_site)))) } +fn bridge_family_modules() -> List { + v1_interpreter_authored_roster_arms() + |> filter(r => match r.dispatch_emit_site { EvalCallBridgeFamilySite { module: _ } => true, _ => false }) + |> map(r => match r.dispatch_emit_site { + EvalCallBridgeFamilySite { module: m } => qualified_name_to_dotted_string(qn: m), + _ => "" + }) +} + +fn distinct_bridge_family_module_count() -> Int { + count(gunbc.v1_interpreter_dispatch_emit.distinct_strings(xs: bridge_family_modules())) +} + fn bridge_family_sites_are_split_per_family_red_control() -> Bool { let node_key = dispatch_emit_site_key(site: EvalCallBridgeFamilySite { module: qualified_name_from_dotted_string(dotted: "v2.std.node") }) let lexing_key = dispatch_emit_site_key(site: EvalCallBridgeFamilySite { module: qualified_name_from_dotted_string(dotted: "v2.std.compilers.lexing") }) - distinct_bridge_family_site_count() == 9 && node_key != lexing_key + distinct_bridge_family_module_count() > 1 + && distinct_bridge_family_site_count() == distinct_bridge_family_module_count() + && node_key != lexing_key } fn live_roster_has_no_rust_variant_collisions() -> Bool { diff --git a/dag/test/claim/v1_interpreter_primitive_roster_acceptance_test.dag b/dag/test/claim/v1_interpreter_primitive_roster_acceptance_test.dag index b67922a0682..e75dbb81390 100644 --- a/dag/test/claim/v1_interpreter_primitive_roster_acceptance_test.dag +++ b/dag/test/claim/v1_interpreter_primitive_roster_acceptance_test.dag @@ -58,9 +58,7 @@ fn duplicate_row_keys_refuse() -> Bool { fn shadows_are_exactly_the_known_named_set() -> Bool { let free = shadowed_spellings(rows: v1_interpreter_primitive_arms() |> filter(r => r.form == FreeCall)) let method = shadowed_spellings(rows: v1_interpreter_primitive_arms() |> filter(r => r.form == MethodCall)) - count(free) == 2 - && (free |> any(x => x == "inert_lens_unreached_module_count")) - && (free |> any(x => x == "inert_lens_top_level_module_count")) + count(free) == 0 && count(method) == 1 && (method |> all(x => x == "lookup")) && !form_has_no_shadowed_spelling(rows: [ diff --git a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag index 98f88e88297..98213bddc34 100644 --- a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag +++ b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag @@ -104,9 +104,8 @@ test fn duplicate_detector_admits_one_spelling_at_two_distinct_sites() -> Bool { count(duplicate_row_keys(rows: planted)) == 0 } -test fn free_call_shadowing_is_exactly_the_two_inert_lens_bridges() -> Bool { - let s = shadowed_spellings(rows: v1_interpreter_primitive_arms() |> filter(r => r.form == FreeCall)) - count(s) == 2 && (s |> any(x => x == "inert_lens_unreached_module_count")) && (s |> any(x => x == "inert_lens_top_level_module_count")) +test fn free_call_carries_no_shadowed_spelling() -> Bool { + form_has_no_shadowed_spelling(rows: v1_interpreter_primitive_arms() |> filter(r => r.form == FreeCall)) } test fn method_call_shadowing_is_exactly_the_known_lookup_case() -> Bool { diff --git a/docs/plans/axiom-syllogism-lens.md b/docs/plans/axiom-syllogism-lens.md index ffa565811bf..2995c71bbb0 100644 --- a/docs/plans/axiom-syllogism-lens.md +++ b/docs/plans/axiom-syllogism-lens.md @@ -130,7 +130,7 @@ The witness homes at `dag/test/claim/design_argument_witness_test.dag`, floor-di | --- | --- | --- | | acyclicity / cycle detection | `graph_has_multi_node_scc` | `std/graph.dag` | | forward/reverse adjacency, DFS | `forward_adjacency` · `reverse_adjacency` · `dfs_finish_order` | `std/graph.dag` | -| reachability `universe ∖ reachable(roots)` | the inert-lens / doc-graph BFS shape | `inert_lens_modules` (`cli_run.rs`) · `doc_reachability_project.rs` | +| reachability `universe ∖ reachable(roots)` | the inert-lens / doc-graph BFS shape | `doc_reachability_project.rs` (was also `inert_lens_modules`, DELETED gunbc#8141) | | truth-value / syllogistic structure | `Classical = True \| False` | `std/logic.dag` | | well-founded / acyclic grounding | initial-algebra + size-change | `std/induction.dag` | | fail-closed lens verdict carrier | `LensVerdict` (Holds/Violation/NotApplicable/Unrealized) | `std/lens_verdict.dag` | diff --git a/docs/plans/construction-justification-rule.md b/docs/plans/construction-justification-rule.md index 3ee189651f8..273e94f1376 100644 --- a/docs/plans/construction-justification-rule.md +++ b/docs/plans/construction-justification-rule.md @@ -1,6 +1,6 @@ # The construction-justification rule (authoring-time) — §0 -> ROADMAP §0 meta-item. The authoring-time judgment that layers **on top of** the executable #5433 inert-lens backstop. DESIGN refs: §5 (construction over validation; the decidability trichotomy; the "never" trap), §6 ("construction first"; lenses are the residue mechanism; coverage-by-illusion), §7 (the recursion — make the lens discipline itself fail-closed). Sibling frame: [expressibility-frontier.md](expressibility-frontier.md) (the same three regions, generalized). +> **SUPERSEDED IN PART — READ §5 BEFORE §2-§4 (2026-08-11, gunbc#8141).** Both executable halves this plan describes are DELETED: the #5433 inert-lens backstop and the fail-closed construction-justification presence check. Sections 2, 3 and 4 below are retained as the record of what was built and why, NOT as a description of the live floor — nothing in `discover_floor_corpus_rows` blocks an unreached or unjustified lens today. ROADMAP §0 meta-item. The authoring-time judgment that layered **on top of** the (now deleted) executable #5433 inert-lens backstop. DESIGN refs: §5 (construction over validation; the decidability trichotomy; the "never" trap), §6 ("construction first"; lenses are the residue mechanism; coverage-by-illusion), §7 (the recursion — make the lens discipline itself fail-closed). Sibling frame: [expressibility-frontier.md](expressibility-frontier.md) (the same three regions, generalized). ## 1. The rule @@ -14,9 +14,9 @@ DESIGN §6: a lens is **validation** — it concedes the bad state is *writable* This is **not a parallel taxonomy** (§3): the names are DESIGN §5's, which [expressibility-frontier.md](expressibility-frontier.md) §2 generalizes into regions ①/②/③. The single authority for the typed model is `v2.lens.common.construction_justification`. -## 2. Why this layers on the #5433 backstop — and does not supersede it +## 2. Why this layered on the #5433 backstop — and did not supersede it (HISTORICAL) -The two checks cover the same set (`is_top_level_lens_module`) but answer different questions, and both run in `discover_floor_corpus_rows` (the seed floor-discovery walk, not new cemented Rust): +The two checks covered the same set (`is_top_level_lens_module`) but answered different questions, and both ran in `discover_floor_corpus_rows` (the seed floor-discovery walk). Both are deleted as of gunbc#8141 — see §5: - **#5433 inert-lens backstop** — *is this lens wired?* Every `v2.lens.*` module must be reached by a discovered fail-closed witness, or be deleted. Runs over the **corpus**; it is the floor guarantee. - **construction-justification rule** (this) — *should this be a lens at all, and if so why?* Every `v2.lens.*` module must **record** its construction-justification. @@ -28,7 +28,7 @@ A judgment applied at authoring time **executes nothing**, so it can never repla The **judgment** (which class) is human and unstructurable — its *correctness* cannot be machine-verified (deciding decidability is itself ③, see frontier §6). But the **requirement to have recorded a judgment is structurable**, so we make the *missing-justification* state unwritable: - **Carrier (the mark, §3/§6):** every lens module declares `data construction_justification: ConstructionJustification = …` — the judgment lives **on the lens**, not in a parallel ledger. This mirrors the `extdeps_external_authority_anchor` precedent (a fixed-name required decl per module). -- **Fail-closed presence check:** `discover_floor_corpus_rows` captures which lenses carry the decl during its single walk (zero extra IO) and **fails the floor closed** on any top-level lens that does not. A lens stripped of its justification goes **RED** (green-by-execution; discriminating on revert — `construction_justification_hygiene_tests`). +- **Fail-closed presence check (DELETED 2026-08-11, see §5):** `discover_floor_corpus_rows` captured which lenses carry the decl during its single walk and **failed the floor closed** on any top-level lens that did not. A lens stripped of its justification goes **RED** (green-by-execution; discriminating on revert — `construction_justification_hygiene_tests`). So the bad state ("a lens with no recorded reason to be a lens") is unwritable by construction, while the honest residue (is the recorded reason *true*?) stays review — exactly the partition the rule itself prescribes. @@ -36,10 +36,20 @@ So the bad state ("a lens with no recorded reason to be a lens") is unwritable b - `v2.lens.common.construction_justification` — the typed model (`ConstructionClass` + `ConstructionJustification`). - All 35 top-level `v2.lens.*` modules carry a recorded justification (retroactive classification from each lens's existing header — the audit that surfaces any lens that is secretly a `WallNow`). -- Presence check + discriminating tests wired into `discover_floor_corpus_rows`. +- ~~Presence check + discriminating tests wired into `discover_floor_corpus_rows`~~ — **DELETED 2026-08-11 (gunbc#8141), see §5.** - **Vacuity residual — CLOSED.** Every `ConstructionClass` payload is now typed/grounded, no free string survives: the per-justification `rationale` and `RatchetForever`'s `undecidable_because` were removed (unverifiable §6 parallel-ledger prose no consumer reads); `WallAfterGrounding` carries the structured `dissolves_to: ConstructionMechanism`; and `WallNow`'s former free-text `construction` is now `{ mechanism: ConstructionMechanism, authority: DeclarationRef }` — the authority being the *one* `std.decl_ref.DeclarationRef` the disposition/determinism scaffold markers also bind through (no parallel ref type). So 'this lens chains to a real construction' is no longer prose but a **walkable graph property**: a host-side graph-property witness (`wall_now_authority_graph_is_total`) proves every `WallNow` authority resolves to a real top-level decl and goes RED on a planted dangling binding. That witness is a §6 scaffold (host-side resolution) dissolving onto a unified kind-agnostic decl-resolution primitive once exposed to `.dag`. - **Residue / follow-on (honest):** the *correctness* of each recorded class is review, not gated. Modules recorded as `WallNow` (cost, application_serializer) and the support module `affected_set_examples` flag a §3 home question — they are computations/support filed under `v2.lens.*`, not validation lenses; relocating them is out of scope here (it touches module resolution) and is left as a marked follow-up. +## 5. Enforcement deleted (2026-08-11, gunbc#8141) + +Both executable checks described above ran inside floor witness discovery, and both answered a question about who authored a lens by acquiring a **whole-corpus module graph**. Every discovery run paid that acquisition. Split by era, since the population changed underneath this plan: before gunbc#8140 the roster walk was unconditional, so ordinary CI, regen, the falsifier cadence and every coordinated worker all paid; #8140 made it demand-directed and regen stopped paying; from there to gunbc#8141 the two censuses burdened every remaining discovery-bearing execution — all of which wanted a witness roster and nothing else. That is the DESIGN §6 cost-shape defect in its clearest form: the unit of computation was the world, the unit of fact was one module's authorship, and no consumer of either census justified the price. The inert-lens half additionally reported through two host builtins whose entire `.dag` surface was a pair of self-recursive stubs reachable only because the interpreter intercepted the spelling. + +**What that costs, stated as a regression rather than implied.** A newly authored lens with no discovered witness, and a lens recording no `construction_justification`, are both writable again and **nothing detects either**. The 35-module population §4 reports as fully classified is a historical measurement, not a maintained invariant — a lens added tomorrow with no justification lands green. The obligation survives only as review diligence, which is strictly weaker than the check it replaces, and this plan is not evidence that it holds. + +**Next-rung trigger.** An authorship fact belongs on the module's own declaration, checked at ingestion where that module is already parsed — one module's facts derived from one module's source — rather than reconstructed corpus-wide by a consumer that wanted something else. The `data construction_justification` carrier §3 describes is already the right shape for that; what was wrong was where the check ran, not where the fact lives. Until that lands the class sits at *mitigatable* under DESIGN §4b, declared here so it stays rankable. + +What survived the deletion: `v2.lens.common.construction_justification` (the typed model), every lens module's recorded `construction_justification` decl, and `wall_now_authority_graph_is_total` — the WallNow authority-resolution witness, which is a separate graph property and still executes. + ## Dissolution trigger (DESIGN §6) -Delete this doc when the construction-justification rule is fully built: v2.lens.common.construction_justification is the single-authority typed model, every top-level v2.lens.* module carries a recorded justification, and the fail-closed presence check plus discriminating tests run in discover_floor_corpus_rows — at which point the rule is a witnessed property of the floor (the vacuity residual and the per-class correctness review being the honest §3-buckets that remain) and this design doc is redundant. +SUPERSEDED TRIGGER (2026-08-11, gunbc#8141): the original condition named the fail-closed presence check running in discover_floor_corpus_rows, and that check is deleted, so the trigger as written can never fire — an unreachable condition is a lifecycle claim that structurally cannot report itself satisfied. Replacement: delete this doc when the construction-justification requirement is re-established at ingestion — the authorship fact checked where the module is already parsed, one module's facts from one module's source, rather than reconstructed corpus-wide by a consumer that wanted a witness roster — at which point the rule is again a witnessed property and this design doc is redundant. Until then the doc is retained as the record of what was built, why it was deleted, and what the repository currently does NOT enforce. diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index 60e428606de..2c0e1c95ebd 100644 --- a/docs/plans/inert-layer-lens.md +++ b/docs/plans/inert-layer-lens.md @@ -62,7 +62,7 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 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 1 — module-level. SUPERSEDED SOURCE (2026-08-11, gunbc#8141): do NOT reuse #5433 — it no longer exists.** `inert_lens_modules` and the whole #5433 floor backstop were DELETED, because that census answered a lens-authorship question by acquiring a whole-corpus module graph inside every floor discovery. Its surviving replacement as the reachability authority is `v2.lens.module_graph` (selection-tier import + reference edges), whose live consumer is affected-set selection; `doc_reachability_project.rs` is the same BFS shape over doc nodes. The paragraph below is retained as the historical design, with its subject repointed: what it describes as "reuse the existing walk" now means "build the walk over the module-graph facts", which is a larger job than it reads. Historically, `inert_lens_modules` computed module-import transitive closure from seed roots and reported 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. @@ -72,7 +72,7 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t ## 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. +- **Inertness is a ① wall candidate.** Reachability is decidable; an inert load-bearing carrier should eventually **fail closed** as #5433 once did for lenses ("an inert lens is a lie" → "an inert load-bearing carrier is a lie") — stated in the past tense because that backstop is deleted (gunbc#8141) and no lens-inertness gate runs today. 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). @@ -80,7 +80,7 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t | need | reuse | file | | --- | --- | --- | -| transitive reachability BFS | `inert_lens_modules` | `cli_run.rs:2558-2606` | +| transitive reachability BFS | `v2.lens.module_graph` selection-tier edges (was `inert_lens_modules`, DELETED gunbc#8141) | `module_graph.dag` + `cli_run.rs` `build_module_graph_facts_live` | | 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 | `v2.std.layer` `LayerImportFact` projection | `layer.dag` + `cli_run.rs:layer_import_facts` | @@ -90,7 +90,7 @@ The reading: the **schedule/width** arm of the realization layer is now wired; t - 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. +- **Load-bearing seed caveat:** Tier 1 touches `cli_run.rs` — a DESIGN-named load-bearing file → **escalate before editing**. The former advice here was to extend `inert_lens_modules` behind a flag rather than fork it; that function is DELETED (gunbc#8141) and there is nothing to extend. Whatever Tier 1 becomes, it must not reintroduce a corpus-wide walk inside floor discovery — that placement, not the walk, is what the deletion removed. - **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) @@ -113,7 +113,7 @@ The same three conditions (§1.1) decide the doc wall: **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.) -**LANDED — the doc-graph wall is live (gunbc#5484), with one premise correction.** The "no host bridges" claim above holds **only for the dangling half**. The *orphan* half is `universe ∖ reachable`, and the universe is `docs/**/*.md` — which requires filesystem **enumeration**, and there is no list-dir host effect in `.dag` today (`std/filesystem` exposes only `Read`/`Write`). So the orphan half is host-fed: `src/v1/stage0/src/doc_reachability_project.rs` walks the tree and exposes two scalar verdicts (`doc_graph_orphan_count` / `doc_graph_dangling_link_count`) through the same additive corpus-gate builtin seam as `extdeps_external_authority_live_clean_tree_holds` / `fact_cardinality_*` (it does **not** touch `cli_run.rs`'s #5433 closure). The reachability primitive is the **same BFS shape** as `inert_lens_modules` re-expressed over doc nodes — the §3-single-authority doc *instance* of the one rule, not a forked concept. The dangling half alone *is* expressible in pure `.dag` (`filesystem_read` BFS from roots). **DISSOLUTION TRIGGER:** when `.dag` gains list-dir / compile-graph access (gunbc#5364, the Tier-2 note), the dir-walk + BFS fold into a pure `.dag` reader and the Rust census deletes. Re-derived against the **live** tree at landing: **22 docs, 22 reachable, 0 orphans, 0 dangling** — clean, because this PR added the five missing inbound links + a `docs/runbooks/README.md` index root (the runbook-kind root) and linked the runbook from it. Witness: `dag/test/claim/doc_reachability_witness_test.dag` (floor-discovered `test fn`s, fail-closed, RED on revert); RED/GREEN controls over a synthetic graph in the project module's unit tests. +**LANDED — the doc-graph wall is live (gunbc#5484), with one premise correction.** The "no host bridges" claim above holds **only for the dangling half**. The *orphan* half is `universe ∖ reachable`, and the universe is `docs/**/*.md` — which requires filesystem **enumeration**, and there is no list-dir host effect in `.dag` today (`std/filesystem` exposes only `Read`/`Write`). So the orphan half is host-fed: `src/v1/stage0/src/doc_reachability_project.rs` walks the tree and exposes two scalar verdicts (`doc_graph_orphan_count` / `doc_graph_dangling_link_count`) through the same additive corpus-gate builtin seam as `extdeps_external_authority_live_clean_tree_holds` / `fact_cardinality_*` (it does **not** touch `cli_run.rs`'s #5433 closure). The reachability primitive is the **same BFS shape** as the then-live `inert_lens_modules` (DELETED gunbc#8141) re-expressed over doc nodes — the §3-single-authority doc *instance* of the one rule, not a forked concept. The dangling half alone *is* expressible in pure `.dag` (`filesystem_read` BFS from roots). **DISSOLUTION TRIGGER:** when `.dag` gains list-dir / compile-graph access (gunbc#5364, the Tier-2 note), the dir-walk + BFS fold into a pure `.dag` reader and the Rust census deletes. Re-derived against the **live** tree at landing: **22 docs, 22 reachable, 0 orphans, 0 dangling** — clean, because this PR added the five missing inbound links + a `docs/runbooks/README.md` index root (the runbook-kind root) and linked the runbook from it. Witness: `dag/test/claim/doc_reachability_witness_test.dag` (floor-discovered `test fn`s, fail-closed, RED on revert); RED/GREEN controls over a synthetic graph in the project module's unit tests. ## 9. Open diff --git a/src/v1/04_method.dag b/src/v1/04_method.dag index 685a79771d1..545828b68c7 100644 --- a/src/v1/04_method.dag +++ b/src/v1/04_method.dag @@ -160,8 +160,6 @@ fn builtin_function_registry() -> Map { let m = map_insert(m, "test_migration_delete_guard_uncovered_deletes", list_of_type_variable(id: "test_migration_delete_guard_uncovered_delete_elem")) let m = map_insert(m, "inert_carrier_names_live", list_of_type_variable(id: "inert_carrier_name_elem")) let m = map_insert(m, "inert_carrier_declared_count", int_type) - let m = map_insert(m, "inert_lens_unreached_module_count", int_type) - let m = map_insert(m, "inert_lens_top_level_module_count", int_type) let m = map_insert(m, "non_fold_residue_count", int_type) let m = map_insert(m, "non_fold_residue_unrostered_count", int_type) let m = map_insert(m, "non_fold_residue_stale_roster_count", int_type) diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 541cc3dc528..2e3cb38acde 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -10435,8 +10435,9 @@ fn run() -> Result { // that a naming violation should be "the cheapest possible failure"; measured, the // walk is the most expensive phase in the process (5.9 min of a 56.5-min floor, // ~6 min of a ~15-min regen), because the roster producer it calls builds - // module-graph facts, a second strict reference-resolution pass, inert-lens - // reachability and the construction-justification census. A two-node regen plan + // module-graph facts, a second strict reference-resolution pass, and (until + // gunbc#8141 deleted them) inert-lens reachability plus the + // construction-justification census. A two-node regen plan // paid all of it to discover a roster it never reads. The roster is memoized by // request digest (IN_PROCESS_ROSTER_BY_REQUEST), so plans that DO schedule // discovery pay exactly what they paid before — the corpus batch hits the memo diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 6bc8e49cad7..efc410a2582 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -5483,8 +5483,10 @@ pub struct ModuleGraphFactsLive { // Every in-scope `.dag` path the importer walk SAW on disk (whether or not it produced // facts), and every observed path whose content read refused. The producers skip an // unreadable file at scan time, so without these rows a vanished module is - // indistinguishable from an absent one — the fail-open undercount consumers like the - // inert-lens census must refuse on, never absorb (operator review 2026-07-28, PR #7384). + // indistinguishable from an absent one — the fail-open undercount every consumer of these + // facts must refuse on, never absorb (operator review 2026-07-28, PR #7384). The + // inert-lens census this arm was written for is deleted (gunbc#8141); effect-reach + // derivation and the cross-worker snapshot transport are the live consumers. pub(crate) observed_paths: HashSet, pub(crate) read_refusals: Vec<(String, String)>, } @@ -5945,8 +5947,9 @@ pub(crate) fn build_module_graph_facts_live_uncached( // (import-less-but-referencing std files, witnesses that need src/v1 in their pool, the // pre-existing fleet_converge Srv3 red, and homonyms the bright-cat lane must qualify), so the // loader repoint is staged as a separate part after those land. The REFERENCE producer below is - // already live via the inert-lens reach (the strips' documented CI blocker), which is hygiene- - // only and cannot regress a compile. + // was, until gunbc#8141, already live via the inert-lens reach (the strips' documented CI + // blocker); that consumer is deleted, so the reference producer's remaining live readers are + // affected-set selection and the loader closure. // // EDGE SOURCE — the swap `module_graph.dag`'s `dependency_edge_source_migration_note` designates: // "when [the namespace terminal step] lands, `dependency_resolution_facts_live` swaps to the @@ -20945,82 +20948,18 @@ pub fn discover_floor_witness_roster( test_module_hygiene_bridge::check_orphan_helpers_or_err(source_roots)?; let mut rows = invoke_floor_discovery_producer(source_roots, scan_dirs, exclude_substrings)?; rows = apply_discovery_scope_dirs_filter(rows, discovery_scope_dirs); - // ONE module-graph facts build serves effect-reach, the inert-lens reach, and the - // justification census (6A repoint: `build_floor_lens_import_graph`'s second - // corpus scan is deleted; `v2.lens.module_graph` facts are the single - // edge/declaration authority on this path). + // The module-graph facts build now serves exactly two consumers on this path: + // effect-reach derivation below, and the cross-worker snapshot transport in + // `floor_discovery_snapshot::install_floor_discovery_snapshot`. The supply-side + // lens censuses that used to ride along (inert-lens reach, construction-justification) + // are deleted — they made every discovery run acquire a whole-corpus world to answer + // a question about lens authorship. let facts = build_module_graph_facts_live(source_roots); refuse_on_module_graph_read_refusals(&facts)?; apply_effect_reach_derived_reads_live_tree(&mut rows, &facts); - let inert = inert_lens_modules(&rows, &facts); - if !inert.is_empty() { - return Err(format!( - "inert-lens hygiene (DESIGN.md §6): {} lens module(s) under `v2.lens.*` are authored \ - but unreached by any discovered floor witness — an inert lens is a lie. Wire each \ - with a discovered fail-closed witness (a `*_test.dag` `test fn`/`test data`, or a \ - scan-dir `unified_claim_*`) or delete it: {}", - inert.len(), - inert.join(", ") - )); - } - let (lens_module_to_path, lens_with_justification) = lens_justification_census(&facts)?; - let unjustified = unjustified_lens_modules(&lens_module_to_path, &lens_with_justification); - if !unjustified.is_empty() { - return Err(format!( - "construction-justification (DESIGN.md §5/§6): {} lens module(s) under `v2.lens.*` do \ - not record a `construction_justification` — before adding a lens you must justify why \ - the bad-state class cannot be made unwritable by construction. Add a `data \ - construction_justification: ConstructionJustification = …` decl (see \ - v2.lens.common.construction_justification) classifying it as WallNow / \ - WallAfterGrounding / RatchetForever: {}", - unjustified.len(), - unjustified.join(", ") - )); - } Ok(rows) } -fn default_floor_lens_hygiene_excludes() -> Vec { - witness_exclusion_substrings() -} - -/// Floor witness builtin (#5433 sibling to `doc_graph_orphan_count`): unreached top-level -/// `v2.lens.*` module count. Returns `-1` when the corpus walk fails closed. -pub fn inert_lens_unreached_module_count() -> i64 { - let roots = default_source_roots(); - let scan_dirs = witness_discovery_scan_dirs(); - let excludes = default_floor_lens_hygiene_excludes(); - let facts = build_module_graph_facts_live(&roots); - if refuse_on_module_graph_read_refusals(&facts).is_err() { - return -1; - } - match invoke_floor_discovery_producer(&roots, &scan_dirs, &excludes) { - Ok(rows) => inert_lens_modules(&rows, &facts).len() as i64, - Err(_) => -1, - } -} - -/// Floor witness builtin: declared top-level `v2.lens.*` module count (non-vacuity oracle). -pub fn inert_lens_top_level_module_count() -> i64 { - let facts = build_module_graph_facts_live(&default_source_roots()); - if refuse_on_module_graph_read_refusals(&facts).is_err() { - return -1; - } - facts - .nodes - .iter() - .filter(|n| is_top_level_lens_module(&n.module)) - .count() as i64 -} - -fn declares_construction_justification(content: &str) -> bool { - content.lines().any(|line| { - let trimmed = line.trim_start(); - trimmed.starts_with("data construction_justification") - && trimmed.contains("ConstructionJustification") - }) -} - // ITEM 2 (reference grounding): the construction->authority graph witness. // // `WallNow.construction` was free-text prose; it is now @@ -21117,20 +21056,6 @@ pub fn construction_authority_graph_unresolved( )) } -pub(crate) fn unjustified_lens_modules( - module_to_path: &std::collections::HashMap, - justified: &std::collections::BTreeSet, -) -> Vec { - let mut missing: Vec = module_to_path - .keys() - .filter(|m| is_top_level_lens_module(m) && !justified.contains(*m)) - .cloned() - .collect(); - missing.sort(); - missing.dedup(); - missing -} - fn repo_relative_dag_path(path: &str) -> String { let normalized = path.replace('\\', "/"); let ws = workspace_root(); @@ -21142,20 +21067,13 @@ fn repo_relative_dag_path(path: &str) -> String { stripped.trim_start_matches("./").to_string() } -fn is_top_level_lens_module(module: &str) -> bool { - match module.strip_prefix("v2.lens.") { - Some(rest) => !rest.is_empty() && !rest.contains('.'), - None => false, - } -} - -/// Fail-closed arm for every lens-census consumer of the module-graph facts -/// (operator review 2026-07-28, PR #7384): the fact producers skip unreadable files at -/// scan time, so an unreadable top-level lens would otherwise VANISH from both the -/// lens universe (`inert_lens_top_level_module_count`) and the justification census — -/// an absorbing fail-open undercount, not an over-flag. Any read refusal recorded by -/// the single facts authority stops the census, typed and located (paths named), -/// never narrowed. +/// Fail-closed arm for every consumer of the module-graph facts (operator review +/// 2026-07-28, PR #7384): the fact producers skip unreadable files at scan time, so an +/// unreadable module would otherwise VANISH from the facts entirely — an absorbing +/// fail-open undercount, not an over-flag. Any read refusal recorded by the single +/// facts authority stops the build, typed and located (paths named), never narrowed. +/// The lens censuses this arm was first written for are deleted; effect-reach +/// derivation and the cross-worker snapshot transport are the live consumers. pub(crate) fn refuse_on_module_graph_read_refusals( facts: &ModuleGraphFactsLive, ) -> Result<(), String> { @@ -21176,102 +21094,6 @@ pub(crate) fn refuse_on_module_graph_read_refusals( )) } -/// Reachability walk for the inert-lens hygiene census over the module-graph facts -/// SELECTION tier (import edges + strict-tier reference edges) — the same -/// `v2.lens.module_graph` authority affected-set selection reads. 6A repoint: replaces -/// the deleted `build_floor_lens_import_graph`, which re-scanned the whole corpus into -/// a second module-name-grain adjacency beside the facts build the roster already -/// performs. One edge authority, walked at path grain; module names derive from the -/// same facts' declaration rows. The legacy walk also carried undeclared raw import -/// names in its reached set; `build_import_adjacency` drops edges to undeclared -/// targets, and an undeclared name can never be a declared lens module, so the inert -/// set is unchanged (proven by the legacy-oracle equivalence test: -/// `facts_walk_matches_legacy_floor_lens_graph_on_live_corpus`). -pub(crate) fn inert_lens_modules( - rows: &[DiscoveryRow], - facts: &ModuleGraphFactsLive, -) -> Vec { - // Seed reachability from ALL *_test.dag files the facts scan saw (declared modules - // plus edge-bearing importers — a file with neither contributes no module and no - // edges, so omitting it cannot change reachability), not just enrolled rows, so - // witnesses in the execution corpus also count for lens coverage even though they - // are excluded from the main corpus rows. - let mut seeds: BTreeSet = rows - .iter() - .map(|r| repo_relative_dag_path(&r.entry)) - .collect(); - for path in facts - .declared_paths - .iter() - .chain(facts.selection_adjacency.keys()) - { - if path.ends_with("_test.dag") { - seeds.insert(path.clone()); - } - } - let mut reached_paths: HashSet = HashSet::new(); - let mut queue: Vec = Vec::new(); - for path in seeds { - if reached_paths.insert(path.clone()) { - queue.push(path); - } - } - while let Some(path) = queue.pop() { - for target in facts.selection_adjacency.get(&path).into_iter().flatten() { - if reached_paths.insert(target.clone()) { - queue.push(target.clone()); - } - } - } - let reached_modules: HashSet<&String> = reached_paths - .iter() - .filter_map(|p| facts.path_to_module.get(p)) - .collect(); - let mut inert: Vec = facts - .nodes - .iter() - .map(|n| &n.module) - .filter(|m| is_top_level_lens_module(m) && !reached_modules.contains(m)) - .cloned() - .collect(); - inert.sort(); - inert.dedup(); - inert -} - -/// Top-level `v2.lens.*` (module → path) rows from the module-graph facts, plus the -/// subset recording a `construction_justification`. Fail-closed per file: a lens file -/// that cannot be read refuses, never counts as justified (the arm the deleted -/// `build_floor_lens_import_graph` carried for the whole corpus, kept here scoped to -/// the lens declarations — the only file reads left on this census path). -pub(crate) fn lens_justification_census( - facts: &ModuleGraphFactsLive, -) -> Result< - ( - std::collections::HashMap, - std::collections::BTreeSet, - ), - String, -> { - let ws = workspace_root(); - let mut lens_module_to_path: std::collections::HashMap = - std::collections::HashMap::new(); - let mut justified: std::collections::BTreeSet = std::collections::BTreeSet::new(); - for node in &facts.nodes { - if !is_top_level_lens_module(&node.module) { - continue; - } - let rel = workspace_relative_repo_path(&node.path); - let content = - std::fs::read_to_string(ws.join(&rel)).map_err(|e| format!("read {rel}: {e}"))?; - if declares_construction_justification(&content) { - justified.insert(node.module.clone()); - } - lens_module_to_path.insert(node.module.clone(), rel); - } - Ok((lens_module_to_path, justified)) -} - /// Host realization of std.realization_schedule.NodeFrontierSelection (signed design: /// docs/plans/affected-set-differential-falsifier.md). PredictOnly computes would-skip /// per row, RECORDS the prediction, and runs the row anyway — the falsifier cadence @@ -29338,11 +29160,9 @@ mod source_root_ingest_manifest_tests { } #[cfg(test)] -mod inert_lens_hygiene_tests { +mod module_graph_read_refusal_tests { use super::{ build_import_adjacency, build_module_graph_facts_live, default_source_roots, - discover_floor_witness_roster, inert_lens_modules, is_top_level_lens_module, - witness_discovery_scan_dirs, witness_exclusion_substrings, DiscoveryRow, ImportResolutionFactRaw, ModuleDeclarationFactRaw, ModuleGraphFactsLive, }; use std::path::PathBuf; @@ -29355,15 +29175,6 @@ mod inert_lens_hygiene_tests { .to_path_buf() } - fn row(entry: &str, function: &str) -> DiscoveryRow { - DiscoveryRow { - label: function.to_string(), - entry: entry.to_string(), - function: function.to_string(), - reads_live_tree: false, - } - } - /// Synthetic `ModuleGraphFactsLive` through the SAME construction path the live /// build uses (`build_import_adjacency`), so the walk tests exercise real /// adjacency construction, not a parallel hand map. @@ -29412,245 +29223,13 @@ mod inert_lens_hygiene_tests { } } - #[test] - fn top_level_lens_module_predicate() { - assert!(is_top_level_lens_module("v2.lens.effect")); - assert!(is_top_level_lens_module( - "v2.lens.extdeps_shape_transport_policy" - )); - assert!(!is_top_level_lens_module( - "v2.lens.extdeps_shape_transport_policy.module_refs" - )); - assert!(!is_top_level_lens_module( - "v2.test.lens_effect.effect_depends_on" - )); - assert!(!is_top_level_lens_module("v2.std.algebra")); - assert!(!is_top_level_lens_module("v2.lens.")); - } - - #[test] - fn detector_red_on_unreached_green_on_wired() { - // Discriminating RED for the facts-tier walk: an unwired lens flags inert… - let facts = synthetic_facts(&[("v2.lens.demo", "src/v2/lens/demo.dag")], &[]); - let inert = inert_lens_modules(&[], &facts); - assert_eq!(inert, vec!["v2.lens.demo".to_string()]); - - // …wiring a discovered witness clears it… - let facts = synthetic_facts( - &[ - ("v2.lens.demo", "src/v2/lens/demo.dag"), - ( - "v2.test.lens_demo.w", - "src/v2/workflow/lens_demo_family_eval_test.dag", - ), - ], - &[( - "src/v2/workflow/lens_demo_family_eval_test.dag", - "v2.lens.demo", - )], - ); - let rows = vec![row("src/v2/workflow/lens_demo_family_eval_test.dag", "w")]; - assert!( - inert_lens_modules(&rows, &facts).is_empty(), - "wiring a discovered witness must clear the inert flag" - ); - - // …and reachability is transitive through the selection adjacency. - let facts = synthetic_facts( - &[ - ("v2.lens.demo", "src/v2/lens/demo.dag"), - ("v2.lens.sib", "src/v2/lens/sib.dag"), - ( - "v2.test.lens_demo.w", - "src/v2/workflow/lens_demo_family_eval_test.dag", - ), - ], - &[ - ( - "src/v2/workflow/lens_demo_family_eval_test.dag", - "v2.lens.demo", - ), - ("src/v2/lens/demo.dag", "v2.lens.sib"), - ], - ); - assert!( - inert_lens_modules(&rows, &facts).is_empty(), - "a transitively-reached sibling lens must count as wired" - ); - } - - // ── 6A closure repoint receipts ───────────────────────────────────────────── - // - // Legacy oracle, retained TEST-SIDE only (the Phase-1 pattern: - // `resolve_transitively_bfs_legacy`): the deleted `build_floor_lens_import_graph` - // corpus scan + module-name-grain walk, kept to prove the facts-tier walk computes - // the identical inert set and edge relation over the live corpus. - - fn floor_lens_graph_legacy( - source_roots: &[String], - ) -> ( - std::collections::HashMap>, - std::collections::HashMap, - ) { - let mut path_imports: std::collections::HashMap> = - std::collections::HashMap::new(); - let mut module_to_path: std::collections::HashMap = - std::collections::HashMap::new(); - for root in source_roots { - let mut dag_files: Vec = Vec::new(); - super::collect_dag_files_tolerant(std::path::Path::new(root), &mut dag_files); - dag_files.sort(); - for path in dag_files { - let entry = path.to_string_lossy().into_owned(); - let content = std::fs::read_to_string(&path) - .unwrap_or_else(|e| panic!("read {}: {e}", path.display())); - let rel = super::repo_relative_dag_path(&entry); - if let Some(m) = super::extract_module_path(&content) { - module_to_path.insert(m, rel.clone()); - } - path_imports.insert(rel, super::extract_import_paths(&content)); - } - } - for edge in super::reference_edges_as_import_facts( - &super::reference_resolution_facts(source_roots, source_roots, &[]), - true, - ) { - let importer = super::repo_relative_dag_path(&edge.path); - let entry = path_imports.entry(importer).or_default(); - if !entry.contains(&edge.import_module) { - entry.push(edge.import_module); - } - } - (path_imports, module_to_path) - } - - fn inert_lens_modules_legacy( - rows: &[DiscoveryRow], - path_imports: &std::collections::HashMap>, - module_to_path: &std::collections::HashMap, - ) -> Vec { - let mut reached: std::collections::BTreeSet = std::collections::BTreeSet::new(); - let mut queue: Vec = Vec::new(); - let path_to_module: std::collections::HashMap<&String, &String> = - module_to_path.iter().map(|(m, p)| (p, m)).collect(); - let entry_paths: std::collections::BTreeSet = { - let mut s: std::collections::BTreeSet = rows - .iter() - .map(|r| super::repo_relative_dag_path(&r.entry)) - .collect(); - for path in path_imports.keys() { - if path.ends_with("_test.dag") { - s.insert(path.clone()); - } - } - s - }; - for ep in &entry_paths { - if let Some(module) = path_to_module.get(ep) { - if reached.insert((*module).clone()) { - queue.push((*module).clone()); - } - } - if let Some(imports) = path_imports.get(ep) { - for imp in imports { - if reached.insert(imp.clone()) { - queue.push(imp.clone()); - } - } - } - } - while let Some(module) = queue.pop() { - if let Some(mpath) = module_to_path.get(&module) { - if let Some(imports) = path_imports.get(mpath) { - for imp in imports { - if reached.insert(imp.clone()) { - queue.push(imp.clone()); - } - } - } - } - } - let mut inert: Vec = module_to_path - .keys() - .filter(|m| is_top_level_lens_module(m) && !reached.contains(*m)) - .cloned() - .collect(); - inert.sort(); - inert.dedup(); - inert - } - - #[test] - fn facts_walk_matches_legacy_floor_lens_graph_on_live_corpus() { - let ws = workspace_root(); - std::env::set_current_dir(&ws).expect("chdir to workspace root"); - let roots = default_source_roots(); - let (path_imports, module_to_path) = floor_lens_graph_legacy(&roots); - let facts = build_module_graph_facts_live(&roots); - - // Edge-set equivalence at the grain the walk consumes: (importer path → - // declared target module). The legacy map carries undeclared raw names and the - // facts adjacency carries paths; projected to the shared grain they must agree - // row-for-row. - let mut mismatches: Vec = Vec::new(); - for (path, imports) in &path_imports { - let legacy_targets: std::collections::BTreeSet = imports - .iter() - .filter(|m| module_to_path.contains_key(*m)) - .cloned() - .collect(); - let facts_targets: std::collections::BTreeSet = facts - .selection_adjacency - .get(path) - .into_iter() - .flatten() - .filter_map(|p| facts.path_to_module.get(p).cloned()) - .collect(); - if legacy_targets != facts_targets { - mismatches.push(format!( - "{path}: legacy {legacy_targets:?} vs facts {facts_targets:?}" - )); - } - } - assert!( - mismatches.is_empty(), - "6A repoint: selection-tier edge sets diverged from the legacy corpus scan \ - ({} importer(s)):\n{}", - mismatches.len(), - mismatches.join("\n") - ); - - // Inert-set equivalence (the census answer itself). - let legacy = inert_lens_modules_legacy(&[], &path_imports, &module_to_path); - let repointed = inert_lens_modules(&[], &facts); - assert_eq!( - repointed, legacy, - "6A repoint: facts-tier inert set diverged from the legacy walk" - ); - - // Discriminating RED control: sever the edge tier and the same comparison must - // diverge — proves the equality receipts above can go red on a real divergence. - let mut severed = facts.clone(); - severed.selection_adjacency = super::HashMap::new(); - let inert_severed = inert_lens_modules(&[], &severed); - assert!( - !inert_severed.is_empty(), - "severed-edge control: with no edges some lens must flag inert" - ); - assert_ne!( - inert_severed, legacy, - "severed-edge control must diverge from the legacy answer \ - (the equality receipt discriminates)" - ); - } - - // BLOCKER-1 RED (operator review 2026-07-28): a top-level lens PRESENT in the + // BLOCKER-1 RED (operator review 2026-07-28): a module PRESENT in the // source inventory whose content cannot be read must surface as a counted read - // refusal — never vanish from the lens universe. The bad file is invalid UTF-8, so + // refusal — never vanish from the facts. The bad file is invalid UTF-8, so // `read_to_string` refuses for every uid (a chmod-based probe would pass under // root). #[test] - fn unreadable_lens_is_a_read_refusal_not_an_absence() { + fn unreadable_source_is_a_read_refusal_not_an_absence() { // Scratch roots live INSIDE the workspace (gitignored target/): the walk's // path keys are workspace-anchored and an outside-tree root panics by design. // Pool root and importer root are SEPARATE dirs because the pool's @@ -29708,14 +29287,14 @@ mod inert_lens_hygiene_tests { .any(|f| f.path.ends_with("bad_lens.dag")), "no facts may be fabricated for an unreadable file" ); - // End-to-end: a facts value carrying this observation must STOP the census — - // the lens is present in the inventory, produced no module declaration, and + // End-to-end: a facts value carrying this observation must STOP the build — + // the file is present in the inventory, produced no module declaration, and // the refusal (not absence) is the surfaced state. let mut facts = synthetic_facts(&[("v2.lens.good_probe", "target/x/good.dag")], &[]); facts.observed_paths = observation.observed_paths; facts.read_refusals = observation.read_refusals; let err = super::refuse_on_module_graph_read_refusals(&facts) - .expect_err("census must refuse while a lens-bearing path is unreadable"); + .expect_err("the facts build must refuse while a path is unreadable"); assert!( err.contains("bad_lens.dag"), "refusal must locate the unreadable path: {err}" @@ -29724,9 +29303,11 @@ mod inert_lens_hygiene_tests { // The refusal arm itself: red on a recorded refusal (typed, path named), green on // none — and green over the LIVE corpus (the no-refusal control that keeps the - // arm honest about today's tree). + // arm honest about today's tree). The lens censuses this arm was first written for + // are deleted; effect-reach derivation and the cross-worker snapshot transport are + // the consumers that keep it load-bearing. #[test] - fn census_refuses_on_read_refusals_red_and_green() { + fn facts_build_refuses_on_read_refusals_red_and_green() { let mut facts = synthetic_facts(&[("v2.lens.demo", "src/v2/lens/demo.dag")], &[]); assert!(super::refuse_on_module_graph_read_refusals(&facts).is_ok()); facts.read_refusals.push(( @@ -29734,7 +29315,7 @@ mod inert_lens_hygiene_tests { "permission denied".to_string(), )); let err = super::refuse_on_module_graph_read_refusals(&facts) - .expect_err("a recorded read refusal must stop the census"); + .expect_err("a recorded read refusal must stop the facts build"); assert!( err.contains("src/v2/lens/vanished.dag") && err.contains("fail-closed"), "refusal must be typed and located: {err}" @@ -29753,80 +29334,14 @@ mod inert_lens_hygiene_tests { "live corpus inventory must be non-empty (non-vacuity)" ); } - - // 6A cost receipt: the whole lens census (reach + justification) runs on ONE - // module-graph facts build — the deleted second corpus scan cannot come back - // silently. Uses the same instruments as - // `resolve_transitively_threads_prebuilt_facts_without_rescan`. - #[test] - fn lens_census_single_facts_build_receipt() { - let ws = workspace_root(); - std::env::set_current_dir(&ws).expect("chdir to workspace root"); - let roots = default_source_roots(); - super::reset_module_graph_facts_cache_for_test(); - super::reset_module_graph_facts_build_count_for_test(); - super::reset_import_resolution_facts_call_counts_for_test(); - let facts = build_module_graph_facts_live(&roots); - let _ = inert_lens_modules(&[], &facts); - let (lens_module_to_path, justified) = - super::lens_justification_census(&facts).expect("justification census"); - let _ = super::unjustified_lens_modules(&lens_module_to_path, &justified); - assert_eq!( - super::module_graph_facts_build_count_for_test(), - 1, - "one facts build must serve the whole lens census" - ); - assert_eq!( - super::import_resolution_facts_call_count_for_test(), - 1, - "the census must not trigger a second import-facts corpus scan" - ); - assert_eq!( - super::module_declaration_facts_call_count_for_test(), - 1, - "the census must not trigger a second module-declaration scan" - ); - } - - #[test] - fn builtin_inert_lens_counts_are_green_on_live_corpus() { - let ws = workspace_root(); - std::env::set_current_dir(&ws).expect("chdir to workspace root"); - assert_eq!( - super::inert_lens_unreached_module_count(), - 0, - "every v2.lens.* must be reached by a floor witness" - ); - assert!( - super::inert_lens_top_level_module_count() > 0, - "lens universe must be non-empty (non-vacuity oracle)" - ); - } - - #[test] - fn floor_corpus_has_no_inert_lenses() { - let ws = workspace_root(); - std::env::set_current_dir(&ws).expect("chdir to workspace root"); - let roots = default_source_roots(); - let scan_dirs = witness_discovery_scan_dirs(); - let excludes = witness_exclusion_substrings(); - let result = discover_floor_witness_roster(&roots, &scan_dirs, &excludes, &[]); - assert!( - result.is_ok(), - "floor discovery must succeed — every v2.lens.* is wired or deleted: {}", - result.err().unwrap_or_default() - ); - } } #[cfg(test)] -mod construction_justification_hygiene_tests { +mod construction_authority_graph_tests { use super::{ construction_authority_graph_unresolved, construction_authority_unresolved, - declares_construction_justification, discover_floor_witness_roster, - unjustified_lens_modules, wall_now_authority_refs, witness_exclusion_substrings, + wall_now_authority_refs, }; - use std::collections::BTreeSet; use std::collections::HashMap; use std::path::PathBuf; @@ -29838,72 +29353,6 @@ mod construction_justification_hygiene_tests { .to_path_buf() } - #[test] - fn justification_scan_predicate() { - let with = "module v2.lens.demo\n\ - import v2.lens.common.construction_justification { ConstructionJustification, RatchetForever }\n\ - data construction_justification: ConstructionJustification = ConstructionJustification {\n\ - class: RatchetForever\n\ - }\n"; - assert!(declares_construction_justification(with)); - - assert!(!declares_construction_justification( - "data construction_justification_note: String = \"todo\"\n" - )); - assert!(!declares_construction_justification( - "module v2.lens.demo\ndata other: String = \"z\"\n" - )); - } - - #[test] - fn detector_red_on_missing_green_on_recorded() { - let mut module_to_path: HashMap = HashMap::new(); - module_to_path.insert( - "v2.lens.demo".to_string(), - "src/v2/lens/demo.dag".to_string(), - ); - module_to_path.insert( - "v2.lens.common.construction_justification".to_string(), - "src/v2/lens/common/construction_justification.dag".to_string(), - ); - module_to_path.insert("v2.std.text".to_string(), "src/v2/std/text.dag".to_string()); - - let none: BTreeSet = BTreeSet::new(); - assert_eq!( - unjustified_lens_modules(&module_to_path, &none), - vec!["v2.lens.demo".to_string()], - "an unjustified top-level lens must go RED" - ); - - let mut justified: BTreeSet = BTreeSet::new(); - justified.insert("v2.lens.demo".to_string()); - assert!( - unjustified_lens_modules(&module_to_path, &justified).is_empty(), - "recording a justification must clear the violation" - ); - } - - #[test] - fn floor_corpus_every_lens_is_justified() { - let ws = workspace_root(); - std::env::set_current_dir(&ws).expect("chdir to workspace root"); - let roots = vec![ - ws.join("dag").to_string_lossy().into_owned(), - ws.join("src/v2").to_string_lossy().into_owned(), - ]; - let scan_dirs = vec![ - "dag/test/claim".to_string(), - "src/v2/test/claim/manual".to_string(), - ]; - let excludes = witness_exclusion_substrings(); - let result = discover_floor_witness_roster(&roots, &scan_dirs, &excludes, &[]); - assert!( - result.is_ok(), - "floor discovery must succeed — every v2.lens.* records a construction-justification: {}", - result.err().unwrap_or_default() - ); - } - // ITEM 2 graph-property witness: the construction->authority graph is TOTAL over the // live corpus (every WallNow authority DeclarationRef resolves to a real top-level decl). // Perturb-to-RED: plant a dangling decl_name in any WallNow site -> this flips to a @@ -30945,8 +30394,8 @@ pub(crate) fn module_declaration_facts_call_count_for_test() -> usize { /// The import-facts walk plus what it OBSERVED: every in-scope `.dag` path the walk /// saw on disk, and every path whose content read refused. The skip arm on an /// unreadable file used to be silent (`Err(_) => continue`), which made a vanished -/// module indistinguishable from an absent one — the fail-open undercount the -/// inert-lens census must refuse on (operator review 2026-07-28, PR #7384). One walk, +/// module indistinguishable from an absent one — the fail-open undercount the facts +/// consumers must refuse on (operator review 2026-07-28, PR #7384). One walk, /// projected two ways: `import_resolution_facts` stays the thin fact projection. pub(crate) struct ImportResolutionObservation { pub(crate) facts: Vec, @@ -31039,22 +30488,23 @@ pub fn module_declaration_facts(pool_roots: &[String]) -> Vec1 +// ALL edges (over-load is safe — a superset only compiles extra modules). SELECTION reads +// Qualified + UniqueBare only (dropping AmbiguousBare), so an over-connected graph cannot silently +// widen the selection tier. (The inert-lens reach was the other reader of that tier until gunbc#8141 +// deleted it.) AmbiguousBare is a bare identifier declared in >1 // module; under namespace-only that is a Rule-2 ambiguity the source should qualify. // // Dissolve-on: `symbol_index_fill` (SymbolIndex lane) projects exact, scope-aware reference edges from // the filled containment tree; when that lands, this parse-and-index approximation (which is liberal // on bare-name reference collection — a local binder that shadows a globally-unique declared name -// yields a spurious UniqueBare edge, safe for the loader, tolerated by the inert-lens grain) deletes. +// yields a spurious UniqueBare edge, safe for the loader, tolerated at the selection grain) deletes. #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub enum RefEdgeResolution { Qualified, @@ -31086,7 +30536,7 @@ pub struct ReferenceEdgeRaw { /// The tier is per-CONSUMER and the two are not interchangeable: /// - `false` (keep AmbiguousBare) for the LOADER — over-connection is harmless there, since a /// superset only compiles extra modules. -/// - `true` for SELECTION and the inert-lens reach — over-connection is not a safety problem +/// - `true` for SELECTION — over-connection is not a safety problem /// here, it is what destroys the answer. Measured: at `false` an entry's median closure is /// 1136 of 2240 modules (homonyms fan every referrer across the pool); at `true` it is 96, /// the same order as the import-only baseline's 54. @@ -41806,8 +41256,8 @@ mod import_closure_equivalence_tests { /// Floor witness entry paths enrolled by the source-root `*_test.dag` pass /// (`gunbc.ci_layer_roots.witness_layer_roots`), minus the model exclusion list. - /// Avoids `discover_floor_witness_roster` lens-hygiene work — closure set-identity - /// only needs the witness entry roster, not inert-lens classification. + /// Avoids `discover_floor_witness_roster`'s producer + facts work — closure set-identity + /// only needs the witness entry roster. fn floor_witness_entry_paths_for_oracle() -> BTreeSet { let mut entries = BTreeSet::new(); for root in default_source_roots() { diff --git a/src/v1/stage0/src/cli_run/floor_discovery_snapshot.rs b/src/v1/stage0/src/cli_run/floor_discovery_snapshot.rs index 96db7187351..337995bb3c0 100644 --- a/src/v1/stage0/src/cli_run/floor_discovery_snapshot.rs +++ b/src/v1/stage0/src/cli_run/floor_discovery_snapshot.rs @@ -4,7 +4,7 @@ //! //! | Consumer site | What it reads from the discovery walk | Closed projection | //! |---|---|---| -//! | Pre-plan `discover_floor_witness_roster([], [])` | Naming hygiene, orphan/helpers, producer roster, module-graph facts, inert-lens + construction-justification gates | Full snapshot payload + installed module-graph cache | +//! | Demand-directed `discover_floor_witness_roster([], [])` (runs only when the plan schedules a discovery or scoped-witness batch, gunbc#8140) | Naming hygiene, orphan/helpers, producer roster, module-graph facts, effect-reach derivation | Full snapshot payload + installed module-graph cache | //! | Discovery corpus with `scan_dirs=[]` + explicit entries | Skips roster walk; still calls `build_module_graph_facts_live` on selection/skip paths | Module-graph facts bytes in snapshot (cache install) | //! | Discovery corpus with non-empty `scan_dirs` | Full roster walk for that scan shape | Not covered by pre-plan snapshot (distinct request identity) | //! @@ -586,32 +586,6 @@ pub fn produce_floor_discovery_snapshot( let facts = super::build_module_graph_facts_live_uncached(&request.source_roots); super::refuse_on_module_graph_read_refusals(&facts)?; super::apply_effect_reach_derived_reads_live_tree(&mut rows, &facts); - let inert = super::inert_lens_modules(&rows, &facts); - if !inert.is_empty() { - return Err(format!( - "inert-lens hygiene (DESIGN.md §6): {} lens module(s) under `v2.lens.*` are authored \ - but unreached by any discovered floor witness — an inert lens is a lie. Wire each \ - with a discovered fail-closed witness (a `*_test.dag` `test fn`/`test data`, or a \ - scan-dir `unified_claim_*`) or delete it: {}", - inert.len(), - inert.join(", ") - )); - } - let (lens_module_to_path, lens_with_justification) = super::lens_justification_census(&facts)?; - let unjustified = - super::unjustified_lens_modules(&lens_module_to_path, &lens_with_justification); - if !unjustified.is_empty() { - return Err(format!( - "construction-justification (DESIGN.md §5/§6): {} lens module(s) under `v2.lens.*` do \ - not record a `construction_justification` — before adding a lens you must justify why \ - the bad-state class cannot be made unwritable by construction. Add a `data \ - construction_justification: ConstructionJustification = …` decl (see \ - v2.lens.common.construction_justification) classifying it as WallNow / \ - WallAfterGrounding / RatchetForever: {}", - unjustified.len(), - unjustified.join(", ") - )); - } let roster: Vec = rows.iter().map(row_to_snapshot).collect(); let facts_snapshot = facts_to_snapshot(&facts); let request_identity_digest = request_identity_digest(request)?; diff --git a/src/v1/stage0/src/v1_compiler_infer_method.rs b/src/v1/stage0/src/v1_compiler_infer_method.rs index 6fc8765d49b..46b31ae2b8a 100644 --- a/src/v1/stage0/src/v1_compiler_infer_method.rs +++ b/src/v1/stage0/src/v1_compiler_infer_method.rs @@ -484,16 +484,6 @@ pub fn builtin_function_registry() -> Rc>> { "inert_carrier_declared_count".to_string(), int_type(), ); - let m = v1_rt::rc_map_insert( - m.clone(), - "inert_lens_unreached_module_count".to_string(), - int_type(), - ); - let m = v1_rt::rc_map_insert( - m.clone(), - "inert_lens_top_level_module_count".to_string(), - int_type(), - ); let m = v1_rt::rc_map_insert(m.clone(), "non_fold_residue_count".to_string(), int_type()); let m = v1_rt::rc_map_insert( m.clone(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 02d75eab65a..e7ecc6e867a 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -3823,13 +3823,6 @@ macro_rules! v1_bridge_family_arms { arm "v4_bridge.data_init_decl_facts_live" { "data_init_decl_facts_live" } => crate::coproduct_reflection::eval_data_init_decl_facts_live($ctx, &$args), } - family INERT_LENS_BRIDGE_FNS "v2.lens.inert_lens" - lookup_eval_call_bridge_lens_inert_lens eval_call_bridge__v2_lens_inert_lens_arm { - arm "v4_bridge.inert_lens_unreached_module_count" { "inert_lens_unreached_module_count" } => - Ok(Value::Int(crate::cli_run::inert_lens_unreached_module_count())), - arm "v4_bridge.inert_lens_top_level_module_count" { "inert_lens_top_level_module_count" } => - Ok(Value::Int(crate::cli_run::inert_lens_top_level_module_count())), - } } }; } @@ -12280,13 +12273,6 @@ macro_rules! v1_builtin_arms { crate::cli_run::inert_carrier_declared_count_live(), ))), - arm "free_call.inert_lens_unreached_module_count" { "inert_lens_unreached_module_count" } => Ok(Some(Value::Int( - crate::cli_run::inert_lens_unreached_module_count(), - ))), - arm "free_call.inert_lens_top_level_module_count" { "inert_lens_top_level_module_count" } => Ok(Some(Value::Int( - crate::cli_run::inert_lens_top_level_module_count(), - ))), - arm "free_call.non_fold_residue_count" { "non_fold_residue_count" } => Ok(Some(Value::Int(crate::cli_run::non_fold_residue_count()))), arm "free_call.non_fold_residue_unrostered_count" { "non_fold_residue_unrostered_count" } => Ok(Some(Value::Int( crate::cli_run::non_fold_residue_unrostered_count(), diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index a9afa7c7ca9..44771a45b38 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -115,8 +115,6 @@ pub enum EvalBuiltinArm { FreeCallTestMigrationDeleteGuardUncoveredDeletes, FreeCallInertCarrierNamesLive, FreeCallInertCarrierDeclaredCount, - FreeCallInertLensUnreachedModuleCount, - FreeCallInertLensTopLevelModuleCount, FreeCallNonFoldResidueCount, FreeCallNonFoldResidueUnrosteredCount, FreeCallNonFoldResidueStaleRosterCount, @@ -255,8 +253,6 @@ pub fn lookup_eval_builtin_inner(spelling: &str) -> Option { "test_migration_delete_guard_uncovered_deletes" => Some(EvalBuiltinArm::FreeCallTestMigrationDeleteGuardUncoveredDeletes), "inert_carrier_names_live" => Some(EvalBuiltinArm::FreeCallInertCarrierNamesLive), "inert_carrier_declared_count" => Some(EvalBuiltinArm::FreeCallInertCarrierDeclaredCount), - "inert_lens_unreached_module_count" => Some(EvalBuiltinArm::FreeCallInertLensUnreachedModuleCount), - "inert_lens_top_level_module_count" => Some(EvalBuiltinArm::FreeCallInertLensTopLevelModuleCount), "non_fold_residue_count" => Some(EvalBuiltinArm::FreeCallNonFoldResidueCount), "non_fold_residue_unrostered_count" => Some(EvalBuiltinArm::FreeCallNonFoldResidueUnrosteredCount), "non_fold_residue_stale_roster_count" => Some(EvalBuiltinArm::FreeCallNonFoldResidueStaleRosterCount), @@ -393,8 +389,6 @@ macro_rules! eval_builtin_inner_arm { ("free_call.test_migration_delete_guard_uncovered_deletes") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallTestMigrationDeleteGuardUncoveredDeletes }; ("free_call.inert_carrier_names_live") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallInertCarrierNamesLive }; ("free_call.inert_carrier_declared_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallInertCarrierDeclaredCount }; - ("free_call.inert_lens_unreached_module_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallInertLensUnreachedModuleCount }; - ("free_call.inert_lens_top_level_module_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallInertLensTopLevelModuleCount }; ("free_call.non_fold_residue_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallNonFoldResidueCount }; ("free_call.non_fold_residue_unrostered_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallNonFoldResidueUnrosteredCount }; ("free_call.non_fold_residue_stale_roster_count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallNonFoldResidueStaleRosterCount }; @@ -706,27 +700,6 @@ macro_rules! eval_call_bridge__v2_std_data_index_arm { } #[rustfmt::skip] #[derive(Copy, Clone, Debug, PartialEq, Eq)] -pub enum EvalCallBridgeLensInertLensArm { - V4BridgeInertLensUnreachedModuleCount, - V4BridgeInertLensTopLevelModuleCount, -} - -#[rustfmt::skip] -pub fn lookup_eval_call_bridge_lens_inert_lens(spelling: &str) -> Option { - match spelling { - "inert_lens_unreached_module_count" => Some(EvalCallBridgeLensInertLensArm::V4BridgeInertLensUnreachedModuleCount), - "inert_lens_top_level_module_count" => Some(EvalCallBridgeLensInertLensArm::V4BridgeInertLensTopLevelModuleCount), - _ => None, - } -} - -#[rustfmt::skip] -macro_rules! eval_call_bridge__v2_lens_inert_lens_arm { - ("v4_bridge.inert_lens_unreached_module_count") => { $crate::v1_interpreter_dispatch_generated::EvalCallBridgeLensInertLensArm::V4BridgeInertLensUnreachedModuleCount }; - ("v4_bridge.inert_lens_top_level_module_count") => { $crate::v1_interpreter_dispatch_generated::EvalCallBridgeLensInertLensArm::V4BridgeInertLensTopLevelModuleCount }; -} -#[rustfmt::skip] -#[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum TryV2StdCollectionMapPrimitiveGroundingArm { MapGroundingEmptyMap, MapGroundingMapInsert, diff --git a/src/v2/compiler/source_authority.dag b/src/v2/compiler/source_authority.dag index e8230b0ca5f..9fdbefbcb1f 100644 --- a/src/v2/compiler/source_authority.dag +++ b/src/v2/compiler/source_authority.dag @@ -1101,7 +1101,7 @@ data module_storage_supply_cost_note: String = "Why a host handler rather than d data module_storage_supply_unbound_body_note: String = "The body REFUSES rather than recursing. This declaration is an interface whose realization is a host handler; until host-effect emission binds it, an in-graph caller must be told so, loudly and at once. -It was previously written as an unconditional self-call — fn f(x) { f(x: x) } — which is the shape a host-bound stub takes when the host is expected to intercept before the body ever runs. That is true for the inert_lens stubs, which ARE registered in the interpreter dispatch tables (v1_interpreter.rs), so their bodies are unreachable. It is NOT true here: this op has no dispatch registration, so the body is genuinely reachable and a caller would spin instead of stopping. A hang is the weakest possible failure arm — it is not even a stop, it just never answers, and DESIGN section 5 wants a located refusal (a bounded 'forever' is not an 'unknown' error). Flagged non-blocking by reviews 39741 and 39773; fixed here because the seam was open anyway. +It was previously written as an unconditional self-call — fn f(x) { f(x: x) } — which is the shape a host-bound stub takes when the host is expected to intercept before the body ever runs. That is true for a stub whose spelling IS registered in the interpreter dispatch tables (v1_interpreter.rs), so its body is unreachable. It is NOT true here: this op has no dispatch registration, so the body is genuinely reachable and a caller would spin instead of stopping. A hang is the weakest possible failure arm — it is not even a stop, it just never answers, and DESIGN section 5 wants a located refusal (a bounded 'forever' is not an 'unknown' error). Flagged non-blocking by reviews 39741 and 39773; fixed here because the seam was open anyway. No in-graph caller exists today, so this changes no behavior — it changes what happens the first time one does." diff --git a/src/v2/lens/enforcement/contract.dag b/src/v2/lens/enforcement/contract.dag index 86eeb56855a..663e100acc8 100644 --- a/src/v2/lens/enforcement/contract.dag +++ b/src/v2/lens/enforcement/contract.dag @@ -31,7 +31,6 @@ import v2.lens.registry { lens_registry_v0_host_language_transport_script, lens_registry_v0_identical_variant_payload, lens_registry_v0_inert_carrier, - lens_registry_v0_inert_lens, lens_registry_v0_intent_linearity, lens_registry_v0_interface_summary, lens_registry_v0_languages_consumer_census, @@ -332,15 +331,6 @@ data lens_contract_inert_carrier: LensContract = { boundary: ConstructionJustification { class: WallAfterGrounding { dissolves_to: RealizationDispatch } } } -data lens_contract_inert_lens: LensContract = { - entry: lens_registry_v0_inert_lens, - mode: AuditOnly, - claimed_scope: ScopeRoster { roots: ["dag", "src/v1", "src/v2"] }, - consumer_witness: NoConsumerWitness, - exemptions: [], - boundary: ConstructionJustification { class: WallAfterGrounding { dissolves_to: RealizationDispatch } } -} - data lens_contract_intent_linearity: LensContract = { entry: lens_registry_v0_intent_linearity, mode: AuditOnly, @@ -582,7 +572,6 @@ data lens_contract_registry: List = [ lens_contract_host_language_transport_script, lens_contract_identical_variant_payload, lens_contract_inert_carrier, - lens_contract_inert_lens, lens_contract_intent_linearity, lens_contract_interface_summary, lens_contract_languages_consumer_census, diff --git a/src/v2/lens/enforcement/lens_module_gate.dag b/src/v2/lens/enforcement/lens_module_gate.dag index 01c912f36ce..bd7da968cd3 100644 --- a/src/v2/lens/enforcement/lens_module_gate.dag +++ b/src/v2/lens/enforcement/lens_module_gate.dag @@ -11,7 +11,7 @@ import v2.lens.registry { DocReachability, DuplicateComputation, EffectReach, EmittedBinaryEffectConfinement, FallbackArmCensus, MandatoryTag, ExtdepsShapeTransportPolicy, FactCardinality, FactDensity, FnFamily, Grounding, HostLanguageTransportScript, MetaExecConfinement, - IdenticalVariantPayload, InertCarrier, InertLens, IntentLinearity, InterfaceSummary, + IdenticalVariantPayload, InertCarrier, IntentLinearity, InterfaceSummary, LanguagesConsumerCensus, LeafModelVerification, LifecycleCarrier, LiveReadClassification, MachineShape, MockTotality, MutationAdequacy, NonFoldResidue, ProductionQualificationOriginProbe, RealizationVocabularyContainment, RosterRegistry, ScheduleLens, SimulatedRelationship, StructuralSimilarity, @@ -437,13 +437,6 @@ fn lens_module_gate_surface_for_lens_id(id: LensIdV0, module: String) -> LensInv remedy: RemedyDelete, admission: GenuinelyNewInvariant } - InertLens => LensInvariantSurface { - module: module, - projection: ProjectionImportGraph, - verdict_authority: VerdictLensVerdict, - remedy: RemedyDelete, - admission: GenuinelyNewInvariant - } DocReachability => LensInvariantSurface { module: module, projection: ProjectionDocGraph, diff --git a/src/v2/lens/inert_lens.dag b/src/v2/lens/inert_lens.dag deleted file mode 100644 index c5da0792e85..00000000000 --- a/src/v2/lens/inert_lens.dag +++ /dev/null @@ -1,30 +0,0 @@ -module v2.lens.inert_lens - - -fn inert_lens_unreached_clean_for_count(unreached_count: Int) -> Bool { - unreached_count == 0 -} - -fn inert_lens_universe_nonempty_for_count(module_count: Int) -> Bool { - module_count > 0 -} - -fn inert_lens_unreached_module_count() -> Int { - inert_lens_unreached_module_count() -} - -fn inert_lens_top_level_module_count() -> Int { - inert_lens_top_level_module_count() -} - -fn inert_lens_hygiene_has_no_unreached_modules_holds() -> Bool { - inert_lens_unreached_clean_for_count(unreached_count: inert_lens_unreached_module_count()) -} - -fn inert_lens_hygiene_universe_is_nonempty_holds() -> Bool { - inert_lens_universe_nonempty_for_count(module_count: inert_lens_top_level_module_count()) -} - -data construction_justification: ConstructionJustification = ConstructionJustification { - class: WallAfterGrounding { dissolves_to: RealizationDispatch } -} diff --git a/src/v2/lens/registry.dag b/src/v2/lens/registry.dag index 61c8ef39d4a..2e57904c88d 100644 --- a/src/v2/lens/registry.dag +++ b/src/v2/lens/registry.dag @@ -36,7 +36,6 @@ type LensIdV0 | HostLanguageTransportScript | IdenticalVariantPayload | InertCarrier - | InertLens | IntentLinearity | InterfaceSummary | LanguagesConsumerCensus @@ -252,11 +251,6 @@ data lens_registry_v0_inert_carrier: LensRegistryEntryV0 = { module_path: Bound { path: "v2.lens.inert_carrier" } } -data lens_registry_v0_inert_lens: LensRegistryEntryV0 = { - lens_id: InertLens - module_path: Bound { path: "v2.lens.inert_lens" } -} - data lens_registry_v0_intent_linearity: LensRegistryEntryV0 = { lens_id: IntentLinearity module_path: Bound { path: "v2.lens.intent_linearity" } @@ -412,7 +406,6 @@ data lens_registry_v0: List = [ lens_registry_v0_host_language_transport_script, lens_registry_v0_identical_variant_payload, lens_registry_v0_inert_carrier, - lens_registry_v0_inert_lens, lens_registry_v0_intent_linearity, lens_registry_v0_interface_summary, lens_registry_v0_languages_consumer_census, @@ -577,10 +570,6 @@ fn lens_id_v0_eq(left: LensIdV0, right: LensIdV0) -> Bool { InertCarrier => true _ => false } - InertLens => match right { - InertLens => true - _ => false - } IntentLinearity => match right { IntentLinearity => true _ => false diff --git a/src/v2/lens/registry/sg_claims_test.dag b/src/v2/lens/registry/sg_claims_test.dag index 2abebfd7718..54afadedcc2 100644 --- a/src/v2/lens/registry/sg_claims_test.dag +++ b/src/v2/lens/registry/sg_claims_test.dag @@ -27,7 +27,6 @@ import v2.lens.registry { Idempotency, IdenticalVariantPayload, InertCarrier, - InertLens, IntentLinearity, InterfaceSummary, LanguagesConsumerCensus, @@ -103,7 +102,6 @@ data lens_registry_v0_required_ids: List = [ HostLanguageTransportScript, IdenticalVariantPayload, InertCarrier, - InertLens, IntentLinearity, InterfaceSummary, LanguagesConsumerCensus,