From 89cc8659ca2104b899554490173fba2eed65baee Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 24 Aug 2026 18:25:42 +0000 Subject: [PATCH] The inert-carrier lens's self_tested gate is intended: the excluded class has the opposite remedy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A carrier with no consumer AND no test reference never reaches this lens -- the `!self_tested.contains(name) { continue }` line in `cli_run.rs` `compute_inert_carrier_data` skips it. Established, not assumed: the gate is specified in `gunbc.plans.inert_layer_lens`, which names it "the key" filter that narrows "every staged-ahead carrier" (the model-first discipline) down to the DESIGN §5 coverage-by-illusion trap, and whose retirement condition already owns the excluded class as the still-unbuilt run-root reachability cut (`v2.lens.inert_layer`, `CacheLayerPlan` / `WorkDemand`). The reason it cannot be folded in is the remedy, not the size: an inert row means "modeled ahead of its consumer, tested, awaiting one" and dissolves when a consumer lands; the unreferenced class dissolves the other way -- delete the carrier, or write the missing test and let it land here. Folding it in would file hundreds of rows each asserting a test that does not exist. What was actually missing was the statement of that scope ON THE CARRIER: the lens module said nothing about what it cannot see, so a reader reaching `v2.lens.inert_carrier` could only read it as covering everything unconsumed (DESIGN §6, the mark on the carrier is the authority, not a parallel-ledger doc). Both the producer's gate and the roster now carry it. MEASURED, `dag` + `src/v2` at 32597358f16 on 2026-08-24, by a faithful replication of the producer's own algorithm: 8821 declared carriers, 14 flagged (the roster's exact 14 -- which is what validates the replication), 270 skipped by the gate. A dated observation, not a bound; nothing gates on either number. NO NEW CONTROL WAS ADDED, and that is a finding: the exclusion is ALREADY pinned by an executing control, `green_control_untested_unused_carrier_is_not_flagged`, which plants exactly this carrier and asserts it stays off the roster. I wrote a mirror control first and deleted it as a §2 duplicate. Verified by mutation 2026-08-24: gate present, 12 passed; gate deleted, that one control fails with `got ["Staged"]`, everything else still green. Also repairs an unrelated pre-existing break that made ALL of this unrunnable: the `#[cfg(test)]` `SymbolIndex` literal at `cli_run.rs` was missing `type_head_exposures`, so `cargo test -p v1-compiler --lib` did not compile at HEAD. The Rust suite is not in CI (operator ruling 2026-07-11), which is why it rotted unnoticed. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01LEJxNuFJJMhL84wosxfUBn --- src/v1/stage0/src/cli_run.rs | 20 ++++++++++++++++++++ src/v2/lens/inert_carrier.dag | 22 ++++++++++++++++++++++ 2 files changed, 42 insertions(+) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 5aaf5bbcd5d..b3edbdd3b21 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -34364,6 +34364,25 @@ fn compute_inert_carrier_data(files: &[(String, String)]) -> InertCarrierData { if decl_count.get(name).copied().unwrap_or(0) != 1 { continue; } + // INTENDED SCOPE GATE, not an oversight. This lens answers ONE question -- + // DESIGN §5 coverage-by-illusion: a carrier that a test makes look exercised + // while no production code reads it. A carrier that is referenced by NOTHING, + // test included, is a different class with a different remedy (delete it, or + // write the missing test and let it land here), so it cannot share this + // roster: a roster row means "modeled ahead of its consumer, tested, awaiting + // one", and every one of these would be a row asserting a test that does not + // exist. That class is owned by the still-unbuilt run-root reachability cut + // (gunbc.plans.inert_layer_lens, `v2.lens.inert_layer`), whose retirement + // condition names it. Measured over `dag` + `src/v2` at 32597358f16 on + // 2026-08-24: 8821 declared carriers, 14 flagged here, 270 skipped by this + // line -- the same order the plan predicted for a raw sweep ("hundreds"), + // which is why the two are separate cuts and not one roster. A dated + // observation, not a bound: nothing gates on either number. + // `green_control_untested_unused_carrier_is_not_flagged` below is the + // executing control that keeps this exclusion deliberate rather than latent: + // it plants exactly this carrier and asserts it stays off the roster, so + // deleting this line goes red -- executed both ways 2026-08-24: gate present, + // 12 passed; gate deleted, that one control fails with got ["Staged"]. if !self_tested.contains(name) { continue; } @@ -39761,6 +39780,7 @@ mod peel_alias_fixpoint_termination { global_bare, services: crate::v1_rt::rc_empty_map(), transparent_alias_rep: crate::v1_rt::rc_empty_map(), + type_head_exposures: crate::v1_rt::rc_empty_map(), }); let env = std::rc::Rc::new(crate::v1_compiler_infer_env::TypeEnv { module_path: "".to_string(), diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag index 3b3213a8b81..8ad765e48e7 100644 --- a/src/v2/lens/inert_carrier.dag +++ b/src/v2/lens/inert_carrier.dag @@ -14,6 +14,28 @@ fn inert_row(unit: String, reason: String) -> FrontierRow { frontier_row_path(path: unit, reason: reason, dissolution: inert_carrier_row_dissolve) } +// SCOPE, stated on the carrier rather than only in the plan that specified it: this +// roster holds carriers that are DECLARED + REFERENCED BY A TEST + read by no +// production code. A carrier referenced by nothing at all -- no consumer and no test +// -- is invisible here BY CONSTRUCTION (the self_tested gate in the host producer, +// cli_run.rs compute_inert_carrier_data), and that is intended, not a hole in the +// lens. The reason is the remedy, not the size of the set: an inert row says "modeled +// ahead of its consumer, tested, awaiting one" and dissolves when a consumer lands; +// the unreferenced class dissolves the other way -- delete the carrier, or write the +// missing test and let it land here -- so folding it in would file hundreds of rows +// each asserting a test that does not exist. It is owned by the still-unbuilt +// run-root reachability cut named in gunbc.plans.inert_layer_lens (v2.lens.inert_layer), +// whose retirement condition already carries it; this lens is not its next rung and +// must not be read as covering it. +// +// Measured over the witness layer roots (dag, src/v2) at 32597358f16 on 2026-08-24: +// 8821 declared carriers, 14 flagged here (this roster's exact 14), 270 skipped by +// that gate -- the same order the plan predicted for a raw sweep. A dated observation, not a +// bound -- nothing gates on either number, and the exclusion itself is pinned by an +// executing control in the host producer's unit tests +// (green_control_untested_unused_carrier_is_not_flagged, which plants exactly such a +// carrier and asserts it stays off this roster; executed both ways 2026-08-24 -- +// gate present, 12 passed; gate deleted, that control alone fails), not by the count. data inert_carrier_roster: List = [ inert_row(unit: "DownstreamSupportRoster", reason: "modeled downstream coverage-roster carrier from the extdeps modeling preflight (#7571): it is the declared home for support/coverage rows that an upstream module may not carry, and the plan text names it, but no module constructs or reads one yet"), inert_row(unit: "Attempt", reason: "modeled compute-fabric execution carrier from the terminal-contract slice (#8413): one execution attempt with its lineage, declared ahead of the executor that issues attempts against a grant, and referenced only by fabric_terminal_contract_witness_test so far"),