Lane 7: inert-abstraction lens keystone + non-fold-residue audit (fail-closed walls)

DESIGN.md

@@ -219,7 +219,7 @@ still a violation) · internal review finds missing tests, external review finds
 - model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every
   claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on
   the argument itself; the §7 recursion, with this document as the first target). (operator's next
-  project)
+  project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)
 - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)
 - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is
   modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage

docs/plans/fold-ergonomics.md

@@ -81,13 +81,18 @@ construction, so the per-site arms disappear (exactly what #5428 did for the num
 The deep sub-root is the `Value::Null` split (~131 sites, own runway). The safety axis literally: every
 silent `false` is a deferred bug paid later at interest.
 
-**#3 — the lens backstop** *(cheapest gate; gates #1/#2 so new residue can't merge)*. The
-**inert-abstraction lens** (generalize the inert-lens backstop #5433 from lenses to *all* carriers — flag
-*defined + self-tested + zero non-test consumers*) and the **non-fold-residue audit** (`_ =>` over closed
-coproducts · `unwrap_or_default` in inference · hand-rolled recursion where a fold exists). A pure reader
-over the same `Node` tree (zero substrate edits). Decidable, wall-able. First RED witness =
-`Placement`/`Materialization` (a genuinely-inert carrier — *not* the now-wired `cached_stage`, so the lens
-isn't itself inert).
+**#3 — the lens backstop** *(cheapest gate; gates #1/#2 so new residue can't merge)*. **LANDED** (Lane 7,
+this PR): the **inert-abstraction lens** (`v2.lens.inert_carrier` over `inert_carrier_project.rs`) flags a
+type carrier that is *defined + self-tested + zero real consumer* — DESIGN §5 coverage-by-illusion (the
+`self-tested` gate is what separates it from the project's deliberate model-first staging); and the
+**non-fold-residue audit** (`v2.lens.non_fold_residue` over `non_fold_residue_project.rs`) flags a `match`
+whose scrutinee is a closed-coproduct param carrying a `_ =>` wildcard escape. Both are fail-closed floor
+witnesses (`src/v2/lens/{inert_carrier,non_fold_residue}_test.dag`, green-by-execution through
+`claim_batch`), each walled against a named, shrinking exception roster with a stale-roster ratchet, and
+each proven discriminating by synthetic RED/GREEN host controls (inert→RED, consumed→GREEN; residue→RED,
+total-fold→GREEN). Host-fed today; both fold into pure `.dag` Node-tree readers at gunbc#5364. Remaining
+audit targets (deferred, follow-up): `unwrap_or_default` in inference · hand-rolled recursion where a fold
+exists.
 
 **Start with #1.** It is the most elegant (a root with measured fan-out), it is the prerequisite that
 makes #2 a fold instead of a grind, and it is the only one that changes the default.

docs/plans/inert-layer-lens.md

@@ -227,6 +227,22 @@ revert); RED/GREEN controls over a synthetic graph in the project module's unit
 
 ## 9. Open
 
+- **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.
 - Confirm the run-root set (is `scheduler.dag` the sole runtime, or also the v1 `claim_executor` path?
   the digest census touched both).
 - Decide Tier-1-now vs wait for Tier-2's host bridge so the first landing is symbol-granular (the census

src/v1/05_emit_rust.dag

@@ -1470,7 +1470,7 @@ fn emit_lib_rs_from_files(all_module_files: List<TextFile>, has_compiler_tests:
   )
 
   let hand_maintained_mods = if has_compiler_tests {
-    "\npub mod v1_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;\npub mod wire_value_serialize;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod recorded_fixture;\npub mod cache_purity_oracle;\npub mod doc_reachability_project;\npub mod medium_structure_project;\npub mod extdeps_shape_transport_policy_project;\npub mod fact_cardinality_census;\npub mod import_resolution_project;\npub mod languages_consumer_census;\npub mod layering_imports_project;\npub mod module_path_index;\npub mod transport_script_position_project;"
+    "\npub mod v1_interpreter;\npub mod cli_run;\npub mod rest_transport_facts;\npub mod wire_value_serialize;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod recorded_fixture;\npub mod cache_purity_oracle;\npub mod corpus_lex;\npub mod doc_reachability_project;\npub mod inert_carrier_project;\npub mod medium_structure_project;\npub mod extdeps_shape_transport_policy_project;\npub mod fact_cardinality_census;\npub mod import_resolution_project;\npub mod languages_consumer_census;\npub mod non_fold_residue_project;\npub mod layering_imports_project;\npub mod module_path_index;\npub mod transport_script_position_project;"
   } else {
     ""
   }

src/v1/stage0/src/corpus_lex.rs

@@ -0,0 +1,146 @@
+// Shared corpus walk + lexical normalization for the host-fed census lenses (DESIGN §2/§3: one
+// authority for "what is code text", not a copy per census module). The inert-carrier and
+// non-fold-residue censuses both read the same `.dag` corpus and both need the same string-literal-
+// aware comment stripping; forking either would be the redundancy §2/§3 reject (and would widen the
+// bug surface — a future fix to e.g. raw-string handling would have to be made in two places).
+//
+// Host-fed today; DISSOLUTION: folds into a pure `.dag` Node-tree reader (the compile graph already
+// carries each module's source + node structure) when gunbc#5364 (.dag compile-graph / BindsTo
+// access) lands — at which point the token scan here is replaced by structural Node reads.
+
+use std::path::{Path, PathBuf};
+
+pub(crate) fn workspace_root() -> PathBuf {
+    crate::module_path_index::workspace_root()
+}
+
+pub(crate) fn repo_rel(path: &Path) -> String {
+    let ws = workspace_root();
+    let s = path.to_string_lossy().replace('\\', "/");
+    let prefix = format!("{}/", ws.to_string_lossy().replace('\\', "/"));
+    s.strip_prefix(&prefix)
+        .map(|p| p.to_string())
+        .unwrap_or(s)
+        .trim_start_matches("./")
+        .to_string()
+}
+
+pub(crate) fn is_test_dag(path: &str) -> bool {
+    path.ends_with("_test.dag")
+}
+
+pub(crate) fn collect_dag_files(dir: &Path, out: &mut Vec<PathBuf>) {
+    let entries = match std::fs::read_dir(dir) {
+        Ok(e) => e,
+        Err(_) => return,
+    };
+    for entry in entries.flatten() {
+        let path = entry.path();
+        if path.is_dir() {
+            collect_dag_files(&path, out);
+        } else if path.extension().and_then(|e| e.to_str()) == Some("dag") {
+            out.push(path);
+        }
+    }
+}
+
+/// The live `.dag` corpus: every `*.dag` under `dsl/` + `src/v2/`, keyed by repo-relative path,
+/// sorted and deduped. The two trees match `gunbc.ci_layer_roots` (`witness_layer_roots`).
+pub(crate) fn corpus_dag_files() -> Vec<(String, String)> {
+    let mut paths = Vec::new();
+    for root in ["dsl", "src/v2"] {
+        collect_dag_files(&workspace_root().join(root), &mut paths);
+    }
+    let mut out = Vec::new();
+    for p in paths {
+        let rel = repo_rel(&p);
+        if let Ok(content) = std::fs::read_to_string(&p) {
+            out.push((rel, content));
+        }
+    }
+    out.sort();
+    out.dedup();
+    out
+}
+
+/// Lexically normalize one line: drop the trailing `//` comment AND blank the interior of every
+/// `"..."` string literal (each interior byte → a space, delimiters kept). String-literal awareness
+/// is the single authority for "what is code text": a `//` inside a URL string (`"https://..."`) is
+/// not a comment start, and `_ =>`/`{`/`}`/`|`/an identifier inside a string literal is text, not a
+/// wildcard arm / brace / coproduct separator / consumer — so none of it is read as code by the
+/// downstream scanners. Byte length up to the comment is preserved (interior chars blanked 1:1,
+/// including multi-byte continuation bytes) so byte-offset brace matching stays stable.
+pub(crate) fn strip_line_comment(line: &str) -> String {
+    let bytes = line.as_bytes();
+    let mut out = Vec::with_capacity(bytes.len());
+    let mut in_string = false;
+    let mut escaped = false;
+    let mut i = 0;
+    while i < bytes.len() {
+        let b = bytes[i];
+        if in_string {
+            if escaped {
+                out.push(b' ');
+                escaped = false;
+            } else if b == b'\\' {
+                out.push(b' ');
+                escaped = true;
+            } else if b == b'"' {
+                out.push(b'"');
+                in_string = false;
+            } else {
+                out.push(b' ');
+            }
+        } else if b == b'"' {
+            in_string = true;
+            out.push(b'"');
+        } else if b == b'/' && i + 1 < bytes.len() && bytes[i + 1] == b'/' {
+            break; // real (out-of-string) line comment — drop the rest of the line.
+        } else {
+            out.push(b);
+        }
+        i += 1;
+    }
+    // Only ASCII bytes (space, `"`) or original out-of-string bytes are pushed; every string-interior
+    // byte (incl. multi-byte continuation bytes) is replaced with a space, so the result is valid UTF-8.
+    String::from_utf8(out).expect("strip_line_comment output is valid UTF-8")
+}
+
+/// Net brace depth of one line, comments/strings stripped first (so a `{`/`}` inside a string or
+/// comment does not perturb the count).
+pub(crate) fn brace_delta(line: &str) -> i32 {
+    let c = strip_line_comment(line);
+    c.matches('{').count() as i32 - c.matches('}').count() as i32
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn strip_blanks_string_interior_and_drops_comment() {
+        // `//` inside a string survives as blanked interior; the trailing real comment is dropped.
+        let got = strip_line_comment("data u = \"https://x // y\" // real comment");
+        assert!(got.starts_with("data u = \""));
+        assert!(
+            !got.contains("real comment"),
+            "trailing // comment dropped: {got:?}"
+        );
+        assert!(!got.contains("https"), "string interior blanked: {got:?}");
+        // byte length preserved up to the dropped comment (interior chars → spaces 1:1).
+        assert!(got.len() <= "data u = \"https://x // y\" // real comment".len());
+    }
+
+    #[test]
+    fn brace_delta_ignores_braces_in_strings() {
+        assert_eq!(brace_delta("fn f() {"), 1);
+        assert_eq!(brace_delta("let s = \"{ { {\""), 0);
+        assert_eq!(brace_delta("} // }"), -1);
+    }
+
+    #[test]
+    fn is_test_dag_matches_suffix() {
+        assert!(is_test_dag("src/v2/lens/x_test.dag"));
+        assert!(!is_test_dag("src/v2/lens/x.dag"));
+    }
+}