diff --git a/DESIGN.md b/DESIGN.md index f7dc2f9f8fb..dd7fd282b91 100644 --- a/DESIGN.md +++ b/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 diff --git a/docs/plans/fold-ergonomics.md b/docs/plans/fold-ergonomics.md index c3f6c14d7c1..a9df0b95942 100644 --- a/docs/plans/fold-ergonomics.md +++ b/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. diff --git a/docs/plans/inert-layer-lens.md b/docs/plans/inert-layer-lens.md index 90762c4da9e..485b8118052 100644 --- a/docs/plans/inert-layer-lens.md +++ b/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 diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index 1b411761c16..9c05c0b6042 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -1470,7 +1470,7 @@ fn emit_lib_rs_from_files(all_module_files: List, 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 { "" } diff --git a/src/v1/stage0/src/corpus_lex.rs b/src/v1/stage0/src/corpus_lex.rs new file mode 100644 index 00000000000..277615d9208 --- /dev/null +++ b/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) { + 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")); + } +} diff --git a/src/v1/stage0/src/inert_carrier_project.rs b/src/v1/stage0/src/inert_carrier_project.rs new file mode 100644 index 00000000000..aeb03925ed2 --- /dev/null +++ b/src/v1/stage0/src/inert_carrier_project.rs @@ -0,0 +1,443 @@ +// The inert-abstraction census (Lane 7 — DESIGN.md §5/§6, docs/plans/inert-layer-lens.md, +// docs/plans/fold-ergonomics.md §3). +// +// An "inert carrier" is a declared type carrier (`type X = ...` / `type X { ... }`) that is +// DEFINED, possibly SELF-TESTED, but has ZERO real consumer — DESIGN §5's coverage-by-illusion / +// §6's "the machinery exists but nothing gates on it." This generalizes the #5433 inert-LENS floor +// backstop (which walls unreached `v2.lens.*` modules) to carriers in general. +// +// CONSTRUCTION-FIRST NOTE (DESIGN §5, the construction_justification rule): inertness cannot be made +// unwritable by construction — modeling a carrier ahead of its consumer is the project's deliberate +// model-first discipline, so "must already have a consumer" is not a precondition you can enforce at +// the declaration site. So this is the genuinely-unstructurable residue a lens is for: a decidable +// reachability/consumer property, walled fail-closed against a NAMED, SHRINKING exception roster +// (the realization-loop staged-ahead carriers) — the same ratchet-during-migration → wall-when-empty +// shape as #5433 and the doc-graph reachability wall (doc_reachability_project.rs). +// +// DEFINITION — the COVERAGE-BY-ILLUSION class exactly (bright-stag's deliverable 1 wording: "defined +// + self-tested + ZERO real consumer"): +// A carrier is inert iff (a) it is DECLARED in a non-test file, (b) it is SELF-TESTED — its NAME +// (as a whole identifier token) appears in at least one `*_test.dag` file, and (c) it has ZERO +// real consumer — its name appears in NO non-test `.dag` file other than its own declaring file. +// +// The (b) self-tested gate is what makes this a clean keystone rather than "every unused type": +// the corpus is full of carriers modeled ahead of their consumer (extdeps API surfaces, the +// realization loop) — those are the project's deliberate model-first discipline and are NOT +// coverage-by-illusion. A carrier someone bothered to write a TEST for but nothing consumes is the +// precise §5 trap: it LOOKS covered (a green test) yet drives no production behavior. Comments are +// stripped before tokenizing, so a real consumer means a code reference, never prose (a code use is +// never inside a comment → the self-tested+unconsumed verdict cannot false-flag a genuinely-used +// carrier). +// +// This is host-fed today (no whole-corpus reference enumeration exists in `.dag` — see +// docs/plans/inert-layer-lens.md §3 Tier 2). DISSOLUTION TRIGGER: when `.dag` gains compile-graph / +// reference-edge access (gunbc#5364, the `concept_index` trigger), the token scan folds into a pure +// `.dag` reader over `BindsTo` edges and this Rust census deletes. It does NOT touch cli_run.rs's +// #5433 closure — it is the additive corpus-gate builtin seam (sibling to doc_graph_orphan_count / +// fact_cardinality_*). + +use std::collections::{BTreeMap, BTreeSet}; +use std::sync::OnceLock; + +use crate::corpus_lex::{brace_delta, corpus_dag_files, is_test_dag, strip_line_comment}; + +// The NAMED, SHRINKING exception roster: carriers deliberately modeled ahead of their consumer (the +// realization loop is model-first by design — docs/plans/inert-layer-lens.md §5). Each entry is a +// carrier the live census currently reports inert; the roster empties as the realization loop wires +// each one, at which point the lens flips advisory → fail-closed wall. A NEW inert carrier not on +// this roster reds the floor; a rostered carrier that GAINS a consumer (or is deleted) becomes a +// stale entry that also reds, forcing the roster to shrink (the ratchet). +// +// dissolve-on per entry is tracked in docs/plans/inert-layer-lens.md §2 (the realization-loop +// cache-plan / work-demand / sharding / receipt-digest arms). +const INERT_CARRIER_ROSTER: &[&str] = &[ + // SEEDED FROM THE LIVE CENSUS 2026-06-22 (re-derive with the live_tree gate below). Each is a + // self-tested type carrier whose name appears in exactly its single declaring file plus a + // `*_test.dag` — DESIGN §5 coverage-by-illusion (a green test, no production consumer). + // dissolve-on per entry: wire the real consumer, then DELETE the entry (the stale-roster ratchet + // reds the floor until you do). A NEW self-tested-but-unconsumed carrier not listed here reds. + "AccessPolicy", // dsl/std/access.dag — access-policy model; no authz consumer wired yet. + "CargoDependency", // dsl/extdeps/rust/cargo.dag — Cargo manifest dep row; emit/ingest unwired. + "CargoPackage", // dsl/extdeps/rust/cargo.dag — Cargo manifest package row; unwired. + "FilePermissions", // dsl/extdeps/access/posix.dag — POSIX mode permission carrier; no fs consumer. + "FloorWitnessRow", // src/v2/workflow/affected_set_floor_runner.dag — runner row; self-only. + "GitCliReportedVersion", // dsl/extdeps/git/versioning.dag — git --version parse target; unwired. + "ReactHookSite", // src/v2/extdeps/frameworks/react.dag — React hook-site model; unwired. + "SecretValue", // dsl/std/types.dag — secret-string carrier; no redaction consumer wired. +]; + +/// Extract top-level `type NAME` carrier declarations with their full declaration BLOCK text. +/// Carriers are the type abstractions (coproducts + records + aliases); `data`/`fn`/`service` are +/// values/behavior, out of scope for this keystone. The block runs from the `type` line until the +/// next top-level item (matching the corpus's brace-depth convention, as in fact_cardinality_census). +/// Returning the block lets the consumer count distinguish a carrier's OWN self-references (the +/// declaration, recursive arms) from a real USE elsewhere — including a use by another fn in the same +/// declaring file (a lens-local fact type IS consumed by its lens fn; only a use outside the type +/// block counts). The corpus walk + lexical normalization live in `crate::corpus_lex` (shared with +/// the non-fold-residue census — DESIGN §2/§3: one authority for "what is code text"). +fn type_carrier_blocks(content: &str) -> Vec<(String, String)> { + let lines: Vec<&str> = content.lines().collect(); + let mut out = Vec::new(); + let mut i = 0; + while i < lines.len() { + let trimmed = lines[i].trim_start(); + let Some(rest) = trimmed.strip_prefix("type ") else { + i += 1; + continue; + }; + let name: String = rest + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + if name.is_empty() { + i += 1; + continue; + } + let mut block = String::new(); + block.push_str(lines[i]); + block.push('\n'); + let mut depth = brace_delta(lines[i]); + i += 1; + while i < lines.len() { + let nt = lines[i].trim_start(); + if depth <= 0 { + // At depth 0 the block continues only across a `=`/`|` sum continuation; anything + // else (next item, blank line, prose) ends it. + if !(nt.starts_with('|') || nt.starts_with('=')) { + break; + } + } + block.push_str(lines[i]); + block.push('\n'); + depth += brace_delta(lines[i]); + i += 1; + } + out.push((name, block)); + } + out +} + +/// Whole-identifier tokens in a line (alphanumeric + `_`, not starting with a digit boundary issue — +/// a token is a maximal run of `[A-Za-z0-9_]`; numeric-only runs are harmless, they never match a +/// carrier name). +fn identifier_tokens(line: &str) -> Vec { + let mut out = Vec::new(); + let mut cur = String::new(); + for ch in line.chars() { + if ch.is_ascii_alphanumeric() || ch == '_' { + cur.push(ch); + } else if !cur.is_empty() { + out.push(std::mem::take(&mut cur)); + } + } + if !cur.is_empty() { + out.push(cur); + } + out +} + +/// Count whole-identifier occurrences of `name` in `text` (comments stripped). +fn count_token(text: &str, name: &str) -> i64 { + let mut n = 0i64; + for raw in text.lines() { + for tok in identifier_tokens(&strip_line_comment(raw)) { + if tok == name { + n += 1; + } + } + } + n +} + +struct InertCarrierReport { + /// All declared type carriers (name -> declaring file), declared in non-test files. + declared: BTreeMap, + /// Inert carrier names (self-tested ∧ zero use outside their own declaration block), sorted. + inert: Vec, +} + +/// The census core, over an explicit `(rel_path, content)` corpus — so the live `build_report` and +/// the synthetic discrimination controls run the SAME predicate (DESIGN §5: prove by execution, not +/// by a re-implementation that could drift from production). +fn compute_report(files: &[(String, String)]) -> InertCarrierReport { + // 1. Declaration universe + each carrier's OWN self-reference count (occurrences inside its + // declaration block — the `type` line, recursive arms — which are not uses). + let mut declared: BTreeMap = BTreeMap::new(); + let mut decl_count: BTreeMap = BTreeMap::new(); + let mut self_block_refs: BTreeMap = BTreeMap::new(); + for (rel, content) in files { + if is_test_dag(rel) { + continue; + } + for (name, block) in type_carrier_blocks(content) { + declared.entry(name.clone()).or_insert_with(|| rel.clone()); + *decl_count.entry(name.clone()).or_insert(0) += 1; + *self_block_refs.entry(name.clone()).or_insert(0) += count_token(&block, &name); + } + } + + // 2. Total occurrences across non-test files (real-consumer candidates), and self-tested set. + let names: BTreeSet = declared.keys().cloned().collect(); + let mut nontest_occ: BTreeMap = BTreeMap::new(); + let mut self_tested: BTreeSet = BTreeSet::new(); + for (rel, content) in files { + let mut local: BTreeMap = BTreeMap::new(); + for raw in content.lines() { + for tok in identifier_tokens(&strip_line_comment(raw)) { + if names.contains(&tok) { + *local.entry(tok).or_insert(0) += 1; + } + } + } + if is_test_dag(rel) { + for (k, _) in local { + self_tested.insert(k); + } + } else { + for (k, v) in local { + *nontest_occ.entry(k).or_insert(0) += v; + } + } + } + + // 3. Inert = declared exactly once (a doubly-declared name cross-references itself → not flagged, + // the conservative direction) ∧ self-tested ∧ used by ZERO non-test code outside its own + // declaration block. `external_uses = total non-test occurrences − own-block self-references`. + let mut inert: Vec = Vec::new(); + for name in declared.keys() { + if decl_count.get(name).copied().unwrap_or(0) != 1 { + continue; + } + if !self_tested.contains(name) { + continue; // not self-tested → merely-unused (model-first), not coverage-by-illusion. + } + let total = nontest_occ.get(name).copied().unwrap_or(0); + let own = self_block_refs.get(name).copied().unwrap_or(0); + if total - own <= 0 { + inert.push(name.clone()); + } + } + inert.sort(); + inert.dedup(); + InertCarrierReport { declared, inert } +} + +/// Memoized live-tree report. The on-disk corpus is fixed for a process's lifetime, so the four +/// `inert_carrier_*_count` builtins (called one-by-one per witness eval) and the live-tree tests share +/// a single `dsl/` + `src/v2/` walk + report instead of re-walking per call. The pure `compute_report` +/// is left taking `&[files]` so the synthetic RED/GREEN controls keep driving it with in-memory corpora +/// (which never touch this cache). +fn build_report() -> &'static InertCarrierReport { + static REPORT: OnceLock = OnceLock::new(); + REPORT.get_or_init(|| compute_report(&corpus_dag_files())) +} + +/// Count of all carriers the census judges inert (defined + zero real consumer). Includes rostered +/// staged-ahead carriers — this is the raw census, not the gate. +pub fn inert_carrier_count() -> i64 { + build_report().inert.len() as i64 +} + +/// The fail-closed GATE: inert carriers NOT on the named exception roster. A new inert carrier reds +/// the floor; zero means every inert carrier is an acknowledged staged-ahead one. +pub fn inert_carrier_unrostered_count() -> i64 { + let roster: BTreeSet<&str> = INERT_CARRIER_ROSTER.iter().copied().collect(); + build_report() + .inert + .iter() + .filter(|n| !roster.contains(n.as_str())) + .count() as i64 +} + +/// The RATCHET: rostered carriers that are no longer inert (gained a real consumer) or no longer +/// declared (deleted). A stale entry reds the floor, forcing the roster to shrink as the realization +/// loop wires each carrier. +pub fn inert_carrier_stale_roster_count() -> i64 { + let report = build_report(); + let inert: BTreeSet<&String> = report.inert.iter().collect(); + INERT_CARRIER_ROSTER + .iter() + .filter(|n| !inert.contains(&n.to_string())) + .count() as i64 +} + +/// Total declared type carriers (oracle against a read_dir / parse fail-open: zero here would mean +/// the corpus walk silently found nothing). +pub fn inert_carrier_declared_count() -> i64 { + build_report().declared.len() as i64 +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn type_carrier_blocks_extracts_names_and_bodies() { + let c = "module m\ntype Connective = Atom | Conj\ntype WorkDemand {\n field: Int\n}\nfn f() -> Int { 1 }\n"; + let blocks = type_carrier_blocks(c); + let names: Vec<&String> = blocks.iter().map(|(n, _)| n).collect(); + assert_eq!(names, vec!["Connective", "WorkDemand"]); + // The WorkDemand block must include its `}` line but stop before `fn f`. + let wd = &blocks.iter().find(|(n, _)| n == "WorkDemand").unwrap().1; + assert!(wd.contains("field: Int") && wd.contains('}')); + assert!(!wd.contains("fn f")); + } + + #[test] + fn identifier_tokens_are_whole_words() { + // Placement must NOT match inside PlacementSupply (word-boundary discrimination). + let toks = identifier_tokens(" field: PlacementSupply = foo(Placement)"); + assert!(toks.contains(&"PlacementSupply".to_string())); + assert!(toks.contains(&"Placement".to_string())); + assert!(toks.contains(&"field".to_string())); + } + + // The DISCRIMINATING controls (DESIGN §5: green-by-execution, RED on a real defect). They run + // the PRODUCTION predicate (`compute_report`) over a synthetic in-memory corpus, so the + // discrimination is proven on the same code main ships. + fn report_of(files: &[(&str, &str)]) -> Vec { + let owned: Vec<(String, String)> = files + .iter() + .map(|(p, c)| (p.to_string(), c.to_string())) + .collect(); + compute_report(&owned).inert + } + + #[test] + fn red_control_self_tested_zero_consumer_carrier_is_inert() { + // A carrier defined + SELF-TESTED but mentioned in NO other non-test file → inert (RED: the + // lens fires). This is coverage-by-illusion: a green test, no production consumer. + let inert = report_of(&[ + ("a.dag", "module a\ntype Lonely { x: Int }\n"), + ( + "a_test.dag", + "module t\nfn t() -> Bool { Lonely { x: 1 } == Lonely { x: 1 } }\n", + ), + ]); + assert!( + inert.contains(&"Lonely".to_string()), + "a self-tested carrier with no real consumer must be flagged inert; got {inert:?}" + ); + } + + #[test] + fn green_control_carrier_with_real_consumer_is_not_inert() { + // Same carrier, now mentioned in a second non-test file → NOT inert (GREEN: the lens stays + // silent). The ONLY difference from the RED control is a real consumer — the discrimination. + let inert = report_of(&[ + ("a.dag", "module a\ntype Used { x: Int }\n"), + ( + "b.dag", + "module b\nimport a { Used }\nfn f(u: Used) -> Int { u.x }\n", + ), + ( + "a_test.dag", + "module t\nfn t() -> Bool { Used { x: 1 } == Used { x: 1 } }\n", + ), + ]); + assert!( + !inert.contains(&"Used".to_string()), + "a carrier with a real (non-test, cross-file) consumer must NOT be flagged; got {inert:?}" + ); + } + + #[test] + fn green_control_same_file_consumer_is_not_inert() { + // A lens-local fact type: declared AND consumed by a fn in the SAME file (outside its type + // block), plus self-tested. It is genuinely load-bearing (the lens reads it) → NOT inert. + // This is the discrimination the use-outside-block rule buys over a declaring-file exclusion. + let inert = report_of(&[ + ( + "lens.dag", + "module lens\ntype LocalFact { x: Int }\nfn clean(fs: LocalFact) -> Bool { fs.x == 0 }\n", + ), + ("lens_test.dag", "module t\nfn t() -> Bool { clean(fs: LocalFact { x: 0 }) }\n"), + ]); + assert!( + !inert.contains(&"LocalFact".to_string()), + "a carrier consumed by a fn in its own file is NOT inert; got {inert:?}" + ); + } + + #[test] + fn green_control_untested_unused_carrier_is_not_flagged() { + // A carrier with NEITHER a test NOR a consumer is merely-unused (model-first staging), NOT + // coverage-by-illusion. The self-tested gate excludes it — this keeps the wall off the + // project's deliberate ahead-of-consumer modeling (extdeps surfaces, the realization loop). + let inert = report_of(&[("a.dag", "module a\ntype Staged { x: Int }\n")]); + assert!( + !inert.contains(&"Staged".to_string()), + "an untested unused carrier must NOT be flagged (it is model-first, not illusion); got {inert:?}" + ); + } + + #[test] + fn comment_reference_is_not_a_real_consumer() { + // A mention only in another file's COMMENT is not a code consumer (comments are stripped), + // so a self-tested carrier referenced elsewhere only in prose is still inert. A code use can + // never live in a comment, so this never false-flags a genuinely-used carrier. + let inert = report_of(&[ + ("a.dag", "module a\ntype Noted { x: Int }\n"), + ( + "b.dag", + "module b\n// Noted is described here\nfn f() -> Int { 1 }\n", + ), + ( + "a_test.dag", + "module t\nfn t() -> Bool { Noted { x: 1 } == Noted { x: 1 } }\n", + ), + ]); + assert!(inert.contains(&"Noted".to_string())); + } + + #[test] + fn doubly_declared_name_is_not_flagged() { + // A name declared in two files cross-references itself → conservatively not inert. + let inert = report_of(&[ + ("a.dag", "module a\ntype Dup { x: Int }\n"), + ("b.dag", "module b\ntype Dup { y: Int }\n"), + ]); + assert!(!inert.contains(&"Dup".to_string())); + } + + // LIVE-TREE gates. These run over the real corpus and must hold on main; they are the executable + // floor the `.dag` witness mirrors. + #[test] + fn live_tree_declared_universe_is_nonempty() { + assert!( + inert_carrier_declared_count() > 0, + "expected non-empty type-carrier universe; zero means the corpus walk fail-opened" + ); + } + + #[test] + fn live_tree_no_unrostered_inert_carrier() { + let report = build_report(); + let roster: BTreeSet<&str> = INERT_CARRIER_ROSTER.iter().copied().collect(); + let unrostered: Vec<&String> = report + .inert + .iter() + .filter(|n| !roster.contains(n.as_str())) + .collect(); + assert!( + unrostered.is_empty(), + "new inert carrier(s) not on the exception roster (wire a consumer, or add to \ + INERT_CARRIER_ROSTER with a dissolve-on): {unrostered:?}" + ); + } + + #[test] + fn live_tree_roster_has_no_stale_entries() { + let report = build_report(); + let inert: BTreeSet<&String> = report.inert.iter().collect(); + let stale: Vec<&&str> = INERT_CARRIER_ROSTER + .iter() + .filter(|n| !inert.contains(&n.to_string())) + .collect(); + assert!( + stale.is_empty(), + "roster entries that are no longer inert (gained a consumer or were deleted) — remove \ + them so the roster shrinks: {stale:?}" + ); + } +} diff --git a/src/v1/stage0/src/lib.rs b/src/v1/stage0/src/lib.rs index b4597308d7a..243adffb931 100644 --- a/src/v1/stage0/src/lib.rs +++ b/src/v1/stage0/src/lib.rs @@ -13,6 +13,7 @@ pub mod cache_purity_oracle; pub mod cli_run; pub mod coproduct_reflection; +pub mod corpus_lex; pub mod doc_reachability_project; pub mod extdeps_cargo; pub mod extdeps_languages_dag_emit; @@ -30,10 +31,12 @@ pub mod extdeps_languages_rust_types; pub mod extdeps_shape_transport_policy_project; pub mod fact_cardinality_census; pub mod import_resolution_project; +pub mod inert_carrier_project; pub mod languages_consumer_census; pub mod layering_imports_project; pub mod medium_structure_project; pub mod module_path_index; +pub mod non_fold_residue_project; pub mod recorded_fixture; pub mod resolved_graph_cache; pub mod rest_transport_facts; diff --git a/src/v1/stage0/src/non_fold_residue_project.rs b/src/v1/stage0/src/non_fold_residue_project.rs new file mode 100644 index 00000000000..fc9b53515d3 --- /dev/null +++ b/src/v1/stage0/src/non_fold_residue_project.rs @@ -0,0 +1,624 @@ +// The non-fold-residue audit (Lane 7 — DESIGN.md §6, docs/plans/fold-ergonomics.md §0/§3). +// +// DESIGN §6: "a finished stage is one fold (any non-fold residue is either a named irreducible kernel +// or un-migrated modeling — there is no third)." A fold over a CLOSED coproduct is total by +// construction and has NO `_ =>` wildcard arm; a hand-rolled `match` with a `_ =>` over a closed +// coproduct carries a fail-open escape that a fold would not. So a wildcard arm over a closed +// coproduct is non-fold residue — DESIGN §6's un-migrated modeling, the §0 fail-open shape that +// fold-ergonomics §0 traces "it compiles but nothing works" to. +// +// CONSTRUCTION-FIRST NOTE (DESIGN §5): the by-construction ideal is exhaustiveness-by-default — a +// typechecker that rejects a non-exhaustive / wildcard-over-closed-coproduct match (the §4 +// CoproductExhaustiveness direction). That is a load-bearing typechecker change (escalate) AND a +// wildcard is legitimate over OPEN/primitive domains, so a blanket construction ban is wrong. Until +// exhaustiveness-by-default lands, the residue over CLOSED coproducts is the genuinely-unstructurable +// remainder a lens is for — walled fail-closed against a named, shrinking roster. +// +// DETECTION (conservative, decidable, low-false-positive — chosen to never false-red main): +// Flag a `match` iff its SCRUTINEE is a bare identifier that is a FUNCTION PARAMETER whose declared +// type is a known CLOSED coproduct (`type X = A | B | ...`), AND the match body has a top-level `_` +// wildcard arm (`_ =>`). Bare-param + declared-coproduct-type is the case where the scrutinee type +// is known WITHOUT inference; field accesses / call results / generic params are skipped +// (conservative — fewer flags, never a false positive on an open domain). A `_` used as a field +// placeholder (`Atom { identity: _ }`) is NOT a pattern wildcard (it is not followed by `=>`), so it +// is excluded. +// +// Host-fed today; DISSOLUTION: folds into a pure `.dag` Node-tree reader (match nodes + scrutinee +// type) when exhaustiveness-by-default / compile-graph access lands (gunbc#5364). Additive corpus-gate +// builtin seam, sibling to inert_carrier_* / doc_graph_* — does NOT touch cli_run.rs's #5433 closure. + +use std::collections::{BTreeMap, BTreeSet}; +use std::sync::OnceLock; + +use crate::corpus_lex::{brace_delta, corpus_dag_files, is_test_dag, strip_line_comment}; + +// The NAMED exception roster: `file::fn` sites carrying a wildcard over a closed-coproduct param. +// Per DESIGN §6 each is EITHER (a) un-migrated modeling awaiting its fold OR (b) a named irreducible +// kernel — "there is no third." The wall is that no NEW such site merges unlisted; the ratchet is +// that a roster entry which STOPS being residue (file deleted, or the match migrated to a total fold) +// reds until removed. The two §6 categories dissolve differently, so the roster does NOT shrink +// uniformly to zero: +// (a) un-migrated modeling — e.g. `emit_yaml_value`, the `eval_*_node*` Node-interpreter handlers, +// `dag_grammar_terminal_for_mvp1_*_token` — SHOULD become an exhaustive fold over the +// coproduct; dissolve-on is to migrate the match (delete the wildcard). This subset shrinks. +// (b) named irreducible kernel — the algebraic totals whose off-diagonal IS the residue the §6 +// kernel exemption was written for: `*_eq`/`*_relation_eq`/`*_mode_eq` (the `_ => false` +// off-diagonal), the lattice `*_join`/`*_meet`/`*_combine` and partial-order `*_dominates`, +// the boolean collapses (`exit_ok` = `ExitSuccess => true _ => false`, `program_runtime_bool_*`, +// `is_*`/`float_body_is_nan` predicates). Enumerating every off-diagonal pair would NOT make +// these "more total" — they wall PERMANENTLY and are expected to remain on the roster. +// (A per-entry kernel-vs-un-migrated TAG is deferred to the gunbc#5364 dissolution — the pure `.dag` +// Node-tree reader carries each site's match shape and scrutinee type structurally, so the +// classification is derived, not hand-maintained here, where a mistag would dishonestly mark +// migratable debt as a permanent kernel.) +const NON_FOLD_RESIDUE_ROSTER: &[&str] = &[ + // SEEDED FROM THE LIVE CENSUS 2026-06-22 (re-derive with the live_tree gate below). Each is a + // `file::fn` with a `match { ... _ => ... }` — a wildcard escape over a closed + // coproduct. This is the honest baseline; the wall is that no NEW residue merges. + "dsl/extdeps/formats/yaml.dag::emit_yaml_value", + "dsl/extdeps/languages/markdown.dag::md_nested", + "dsl/gunbc/generated_artifact.dag::artifact_eq", + "dsl/gunbc/generated_artifact.dag::artifact_extra_valid", + "dsl/std/computation.dag::constant_bound_value", + "dsl/std/computation.dag::is_constant_bound", + "dsl/std/effects.dag::create_double_init_collapsible", + "dsl/std/effects.dag::create_effect_is_dedupable", + "dsl/std/effects.dag::key_source_eq", + "dsl/std/encoding.dag::encoding_lattice_join", + "dsl/std/encoding.dag::encoding_lattice_meet", + "dsl/std/filesystem.dag::is_text_encoding", + "dsl/std/induction.dag::compose_sub_value", + "dsl/std/induction.dag::compose_sub_value_relations", + "dsl/std/induction.dag::is_strict_style_structural", + "dsl/std/induction.dag::recursion_shape_eq", + "dsl/std/induction.dag::shrink_factor_eq", + "dsl/std/induction.dag::sub_value_structural_eq", + "dsl/std/reducible.dag::reduce_verdict_combine", + "dsl/std/termination.dag::descent_evidence_lattice_join", + "dsl/std/termination.dag::descent_evidence_lattice_meet", + "dsl/std/termination.dag::promote_to_strict", + "dsl/tools/ci_gates.dag::exit_ok", + "dsl/tools/generated_artifact_gate.dag::exit_ok", + "src/v2/compiler/01_tokenize.dag::lex_try_rules_prefer_longer", + "src/v2/compiler/05_eval.dag::eval_bind_node_eval", + "src/v2/compiler/05_eval.dag::eval_branch_node_eval", + "src/v2/compiler/05_eval.dag::eval_loop_node", + "src/v2/compiler/05_eval.dag::eval_match_node_eval", + "src/v2/compiler/05_eval.dag::eval_transform_node", + "src/v2/compiler/05_eval.dag::eval_value_node", + "src/v2/compiler/05_eval.dag::run_test_claim_assert_decided", + "src/v2/compiler/05_eval.dag::run_test_claim_runtime_assert", + "src/v2/compiler/06_translate.dag::translate_algebra_finalize", + "src/v2/compiler/emit_host.dag::run_test_claim_emit_vs_eval_verdict", + "src/v2/compiler/manual/eval_runtime_mvp.dag::eval_mvp2_arg_is_two_literal", + "src/v2/extdeps/formats/spice_passive_projection.dag::passive_spec_from_component", + "src/v2/extdeps/formats/spice_passive_projection.dag::passive_topology_from_component", + "src/v2/extdeps/languages/dag.dag::dag_grammar_terminal_for_mvp1_bind_token", + "src/v2/extdeps/languages/dag.dag::dag_grammar_terminal_for_mvp1_loop_token", + "src/v2/extdeps/languages/dag.dag::dag_grammar_terminal_for_mvp1_match_token", + "src/v2/extdeps/languages/dag.dag::dag_grammar_terminal_for_mvp1_pick_token", + "src/v2/extdeps/languages/dag.dag::dag_grammar_terminal_for_mvp1_rec_token", + "src/v2/extdeps/runtimes/v2_effect_io_pure.dag::effect_io_pure_backends_match", + "src/v2/lens/complexity.dag::complexity_bound_dominates", + "src/v2/lens/complexity.dag::complexity_bound_from_class", + "src/v2/lens/cost.dag::asymptotic_class_dominates", + "src/v2/lens/cost.dag::multiply_classes", + "src/v2/lens/cost.dag::symbolic_cost_dominates", + "src/v2/lens/cost.dag::symbolic_cost_witness", + "src/v2/lens/cost.dag::symbolic_max", + "src/v2/lens/cost.dag::symbolic_product", + "src/v2/lens/cost.dag::symbolic_sequential", + "src/v2/lens/fact_density.dag::connective_is_kernel_ambient_atom", + "src/v2/lens/idempotency.dag::idempotency_verdict_eq", + "src/v2/lens/ownership.dag::ownership_mode_eq", + "src/v2/lens/parallelism.dag::parallelism_relation_eq", + "src/v2/lens/registry.dag::lens_id_v0_eq", + "src/v2/lens/unused_parameters.dag::use_relation_eq", + "src/v2/program.dag::program_runtime_bool_false", + "src/v2/program.dag::program_runtime_bool_true", + "src/v2/std/compilers/target_model.dag::source_atom_value_as_bool", + "src/v2/std/compilers/target_model.dag::source_atom_value_as_char", + "src/v2/std/compilers/target_model.dag::source_atom_value_as_string", + "src/v2/std/compilers/target_model.dag::source_atom_value_as_symbol", + "src/v2/std/compilers/target_model.dag::target_type_expr_emitted_validate_wire_shape", + "src/v2/std/compilers/target_model.dag::target_use_site_ownership_catalog_lookup_step", + "src/v2/std/effects.dag::key_source_eq", + "src/v2/std/float.dag::float_body_is_nan", + "src/v2/std/probe_selector.dag::diagnostic_interface_kind_eq", + "src/v2/std/qualified_name.dag::qn_fold_step", +]; + +// Corpus walk + lexical normalization (`corpus_dag_files`, `strip_line_comment`, `brace_delta`, +// `is_test_dag`) live in `crate::corpus_lex`, shared with the inert-carrier census — DESIGN §2/§3: +// one authority for "what is code text", not a copy per census module. + +/// Source with every line's `//` comment removed and string-literal interiors blanked (positions +/// within a line up to the comment are preserved; the trailing comment becomes empty). Index-stable +/// enough for brace matching. +fn strip_comments(content: &str) -> String { + content + .lines() + .map(strip_line_comment) + .collect::>() + .join("\n") +} + +/// Closed-coproduct type names: a top-level `type X` whose declaration contains a `|` arm separator +/// (a sum type). Record types (`type X { ... }`) and aliases (`type X = Foo`) are not coproducts. +fn closed_coproduct_names(files: &[(String, String)]) -> BTreeSet { + let mut out = BTreeSet::new(); + for (rel, content) in files { + if is_test_dag(rel) { + continue; + } + let lines: Vec<&str> = content.lines().collect(); + let mut i = 0; + while i < lines.len() { + let trimmed = lines[i].trim_start(); + let Some(rest) = trimmed.strip_prefix("type ") else { + i += 1; + continue; + }; + let name: String = rest + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + if name.is_empty() { + i += 1; + continue; + } + // Gather the decl block (same convention as inert_carrier_project) and check for `|`. + let mut block = String::new(); + block.push_str(&strip_line_comment(lines[i])); + let mut depth = brace_delta(lines[i]); + i += 1; + while i < lines.len() { + let nt = lines[i].trim_start(); + if depth <= 0 && !(nt.starts_with('|') || nt.starts_with('=')) { + break; + } + block.push('\n'); + block.push_str(&strip_line_comment(lines[i])); + depth += brace_delta(lines[i]); + i += 1; + } + if block.contains('|') { + out.insert(name); + } + } + } + out +} + +fn is_ident(s: &str) -> bool { + !s.is_empty() + && s.chars().all(|c| c.is_ascii_alphanumeric() || c == '_') + && !s.chars().next().unwrap().is_ascii_digit() +} + +/// Find the index of the `}` matching the `{` at `open` (bytes; ASCII braces). +fn matching_brace(bytes: &[u8], open: usize) -> Option { + let mut depth = 0i32; + let mut j = open; + while j < bytes.len() { + match bytes[j] { + b'{' => depth += 1, + b'}' => { + depth -= 1; + if depth == 0 { + return Some(j); + } + } + _ => {} + } + j += 1; + } + None +} + +/// Does `body` (a match's `{...}` interior) contain a top-level `_ =>` pattern wildcard — i.e. at +/// brace-depth 0 relative to the body, a `_` token immediately followed by `=>` (allowing spaces)? +/// Depth-0 only, so a nested match's wildcard is attributed to the nested match, not this one. +fn has_top_level_wildcard_arm(body: &str) -> bool { + let bytes = body.as_bytes(); + let mut depth = 0i32; + let mut k = 0; + while k < bytes.len() { + match bytes[k] { + b'{' => depth += 1, + b'}' => depth -= 1, + b'_' => { + // `_` must be a standalone token (not part of an identifier) and at depth 0. + let prev_ok = k == 0 || !is_ident_byte(bytes[k - 1]); + let next_is_ident = k + 1 < bytes.len() && is_ident_byte(bytes[k + 1]); + if depth == 0 && prev_ok && !next_is_ident { + // skip spaces, expect `=>` + let mut m = k + 1; + while m < bytes.len() + && (bytes[m] == b' ' || bytes[m] == b'\n' || bytes[m] == b'\t') + { + m += 1; + } + if m + 1 < bytes.len() && bytes[m] == b'=' && bytes[m + 1] == b'>' { + return true; + } + } + } + _ => {} + } + k += 1; + } + false +} + +fn is_ident_byte(b: u8) -> bool { + b.is_ascii_alphanumeric() || b == b'_' +} + +/// Parse `fn NAME(params) ... {` signatures, returning (fn_name, params: name->bare-type, body_range) +/// over a comment-stripped source. The bare type is the type's head identifier (generics stripped). +struct FnSig { + name: String, + params: BTreeMap, + body: String, +} + +fn parse_fns(src: &str) -> Vec { + let bytes = src.as_bytes(); + let mut out = Vec::new(); + for (start, _) in src.match_indices("fn ") { + // `fn ` must start a token (preceded by whitespace/newline/start). + if start > 0 && is_ident_byte(bytes[start - 1]) { + continue; + } + let after = start + 3; + let name: String = src[after..] + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + if name.is_empty() { + continue; + } + // params between the first `(` after the name and its matching `)`. + let paren_open = match src[after..].find('(') { + Some(p) => after + p, + None => continue, + }; + let paren_close = match matching_paren(bytes, paren_open) { + Some(p) => p, + None => continue, + }; + let params = parse_params(&src[paren_open + 1..paren_close]); + // body: first `{` after `)` to its matching `}`. + let brace_open = match src[paren_close..].find('{') { + Some(b) => paren_close + b, + None => continue, + }; + let brace_close = match matching_brace(bytes, brace_open) { + Some(b) => b, + None => continue, + }; + out.push(FnSig { + name, + params, + body: src[brace_open + 1..brace_close].to_string(), + }); + } + out +} + +fn matching_paren(bytes: &[u8], open: usize) -> Option { + let mut depth = 0i32; + let mut j = open; + while j < bytes.len() { + match bytes[j] { + b'(' => depth += 1, + b')' => { + depth -= 1; + if depth == 0 { + return Some(j); + } + } + _ => {} + } + j += 1; + } + None +} + +/// Parse `name: Type, name2: Type2` into name -> bare-type-head. Generics/brackets stripped. +fn parse_params(s: &str) -> BTreeMap { + let mut out = BTreeMap::new(); + let mut depth = 0i32; + let mut cur = String::new(); + let mut parts: Vec = Vec::new(); + for ch in s.chars() { + match ch { + '<' | '(' | '[' => { + depth += 1; + cur.push(ch); + } + '>' | ')' | ']' => { + depth -= 1; + cur.push(ch); + } + ',' if depth == 0 => parts.push(std::mem::take(&mut cur)), + _ => cur.push(ch), + } + } + if !cur.trim().is_empty() { + parts.push(cur); + } + for part in parts { + let Some((name, ty)) = part.split_once(':') else { + continue; + }; + let name = name.trim(); + let ty_head: String = ty + .trim() + .chars() + .take_while(|c| c.is_ascii_alphanumeric() || *c == '_') + .collect(); + if is_ident(name) && !ty_head.is_empty() { + out.insert(name.to_string(), ty_head); + } + } + out +} + +/// A residue site: a `match { ... _ => ... }` where param is a closed-coproduct type. +fn residue_sites(files: &[(String, String)]) -> Vec { + let coproducts = closed_coproduct_names(files); + let mut out: BTreeSet = BTreeSet::new(); + for (rel, content) in files { + if is_test_dag(rel) { + continue; + } + let src = strip_comments(content); + for sig in parse_fns(&src) { + // scan `match` occurrences in the fn body; resolve scrutinee against this fn's params. + for (mi, _) in sig.body.match_indices("match ") { + if mi > 0 && is_ident_byte(sig.body.as_bytes()[mi - 1]) { + continue; + } + let after = mi + "match ".len(); + let Some(brace_rel) = sig.body[after..].find('{') else { + continue; + }; + let scrut = sig.body[after..after + brace_rel].trim(); + if !is_ident(scrut) { + continue; // not a bare identifier (field access / call) -> skip, conservative. + } + let Some(ty) = sig.params.get(scrut) else { + continue; // scrutinee is not a known param -> skip (no type without inference). + }; + if !coproducts.contains(ty) { + continue; // param is not a closed coproduct -> legitimate / open domain. + } + // brace-match the match body and check for a top-level `_ =>` arm. + let body_bytes = sig.body.as_bytes(); + let brace_abs = after + brace_rel; + let Some(close) = matching_brace(body_bytes, brace_abs) else { + continue; + }; + let body = &sig.body[brace_abs + 1..close]; + if has_top_level_wildcard_arm(body) { + out.insert(format!("{}::{}", rel, sig.name)); + } + } + } + } + out.into_iter().collect() +} + +/// The memoized live-tree census: residue sites + closed-coproduct universe size, both derived from a +/// single `dsl/` + `src/v2/` walk. The on-disk corpus is fixed for a process's lifetime, so the four +/// `non_fold_residue_*_count` builtins (called one-by-one per witness eval) share one walk + scan +/// instead of re-walking per call. The pure `residue_sites` / `closed_coproduct_names` stay taking +/// `&[files]` so the synthetic RED/GREEN controls keep driving them with in-memory corpora. +struct NonFoldReport { + sites: Vec, + coproduct_universe: usize, +} + +fn build_report() -> &'static NonFoldReport { + static REPORT: OnceLock = OnceLock::new(); + REPORT.get_or_init(|| { + let files = corpus_dag_files(); + NonFoldReport { + sites: residue_sites(&files), + coproduct_universe: closed_coproduct_names(&files).len(), + } + }) +} + +pub fn non_fold_residue_count() -> i64 { + build_report().sites.len() as i64 +} + +/// The fail-closed GATE: residue sites NOT on the named exception roster. +pub fn non_fold_residue_unrostered_count() -> i64 { + let roster: BTreeSet<&str> = NON_FOLD_RESIDUE_ROSTER.iter().copied().collect(); + build_report() + .sites + .iter() + .filter(|s| !roster.contains(s.as_str())) + .count() as i64 +} + +/// The RATCHET: roster entries that are no longer residue (migrated to a fold, or deleted). +pub fn non_fold_residue_stale_roster_count() -> i64 { + let live: BTreeSet<&str> = build_report().sites.iter().map(|s| s.as_str()).collect(); + NON_FOLD_RESIDUE_ROSTER + .iter() + .filter(|s| !live.contains(*s)) + .count() as i64 +} + +/// Closed-coproduct universe size — fail-open oracle (zero means the corpus walk found nothing). +pub fn non_fold_residue_coproduct_universe_count() -> i64 { + build_report().coproduct_universe as i64 +} + +#[cfg(test)] +mod tests { + use super::*; + + fn files(pairs: &[(&str, &str)]) -> Vec<(String, String)> { + pairs + .iter() + .map(|(p, c)| (p.to_string(), c.to_string())) + .collect() + } + + #[test] + fn coproduct_index_finds_sums_not_records() { + let f = files(&[( + "t.dag", + "module t\ntype Mode = A | B | C\ntype Rec { x: Int }\ntype Alias = Witness\n", + )]); + let cps = closed_coproduct_names(&f); + assert!(cps.contains("Mode")); + assert!(!cps.contains("Rec")); + assert!(!cps.contains("Alias")); + } + + #[test] + fn red_control_wildcard_over_closed_coproduct_is_residue() { + // A hand-rolled match on a coproduct param with a `_ =>` escape — non-fold residue (RED). + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B | C\nfn f(x: Mode) -> Bool {\n match x {\n A => true\n _ => false\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + sites.contains(&"m.dag::f".to_string()), + "a wildcard over a closed-coproduct param must be flagged; got {sites:?}" + ); + } + + #[test] + fn green_control_total_fold_is_not_residue() { + // The SAME function, exhaustive (no wildcard) — a total fold, NOT residue (GREEN). The only + // difference from the RED control is the `_ =>` arm: the discrimination. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B | C\nfn f(x: Mode) -> Bool {\n match x {\n A => true\n B => false\n C => false\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + !sites.contains(&"m.dag::f".to_string()), + "an exhaustive match (no wildcard) must NOT be flagged; got {sites:?}" + ); + } + + #[test] + fn green_control_wildcard_over_open_domain_is_not_residue() { + // A wildcard over a NON-coproduct param (e.g. a String/primitive) is legitimate, not residue. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B\nfn g(s: String) -> Bool {\n match s {\n \"y\" => true\n _ => false\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + !sites.contains(&"m.dag::g".to_string()), + "a wildcard over an open/primitive domain must NOT be flagged; got {sites:?}" + ); + } + + #[test] + fn green_control_field_placeholder_underscore_is_not_a_wildcard_arm() { + // `_` as a record-field placeholder (`A { v: _ }`) is not a pattern wildcard arm. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A { v: Int } | B { v: Int }\nfn f(x: Mode) -> Int {\n match x {\n A { v: _ } => 1\n B { v: _ } => 2\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + !sites.contains(&"m.dag::f".to_string()), + "field-placeholder `_` is not a wildcard arm; got {sites:?}" + ); + } + + #[test] + fn nested_match_wildcard_is_attributed_to_its_own_match() { + // The outer match on `a` is exhaustive; the inner `match b` carries the wildcard — the fn is + // flagged (it has residue), via the inner match. Confirms depth-0 wildcard attribution finds + // the inner match's escape. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B\nfn eq(a: Mode, b: Mode) -> Bool {\n match a {\n A => match b { A => true _ => false }\n B => match b { B => true _ => false }\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!(sites.contains(&"m.dag::eq".to_string())); + } + + #[test] + fn green_control_wildcard_and_slashes_inside_string_literal_are_ignored() { + // String-literal awareness: a `_ =>` and a `//` that live INSIDE a `"..."` string literal + // are not code. The fn below is a TOTAL fold over `Mode` (arms A and B, no real wildcard); the + // only `_ =>` and `//` appear inside a string. A naive scanner would (a) read the `//` as a + // comment and truncate, and/or (b) read the in-string `_ =>` as a wildcard arm and false-RED. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B\nfn f(x: Mode) -> String {\n match x {\n A => \"see https://x/y and _ => z\"\n B => \"b\"\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + !sites.contains(&"m.dag::f".to_string()), + "`_ =>`/`//` inside a string literal must not be read as code; got {sites:?}" + ); + } + + #[test] + fn red_control_real_wildcard_survives_an_in_string_decoy() { + // Discrimination partner of the green control: the SAME in-string decoy, but now a REAL + // top-level `_ =>` wildcard arm is present too. It must still be flagged — string blanking + // must not suppress genuine residue. + let f = files(&[( + "m.dag", + "module m\ntype Mode = A | B | C\nfn f(x: Mode) -> String {\n match x {\n A => \"see https://x/y and _ => z\"\n _ => \"rest\"\n }\n}\n", + )]); + let sites = residue_sites(&f); + assert!( + sites.contains(&"m.dag::f".to_string()), + "a real wildcard arm must still be flagged despite an in-string decoy; got {sites:?}" + ); + } + + #[test] + fn live_tree_coproduct_universe_is_nonempty() { + assert!( + non_fold_residue_coproduct_universe_count() > 0, + "expected a non-empty closed-coproduct universe; zero means the corpus walk fail-opened" + ); + } + + #[test] + fn live_tree_no_unrostered_non_fold_residue() { + let roster: BTreeSet<&str> = NON_FOLD_RESIDUE_ROSTER.iter().copied().collect(); + let unrostered: Vec = residue_sites(&corpus_dag_files()) + .into_iter() + .filter(|s| !roster.contains(s.as_str())) + .collect(); + assert!( + unrostered.is_empty(), + "new non-fold residue (wildcard over a closed-coproduct param) — migrate to a total fold \ + or add to NON_FOLD_RESIDUE_ROSTER with a dissolve-on: {unrostered:?}" + ); + } + + #[test] + fn live_tree_residue_roster_has_no_stale_entries() { + let live: BTreeSet = residue_sites(&corpus_dag_files()).into_iter().collect(); + let stale: Vec<&&str> = NON_FOLD_RESIDUE_ROSTER + .iter() + .filter(|s| !live.contains(&s.to_string())) + .collect(); + assert!( + stale.is_empty(), + "roster entries that are no longer residue (migrated or deleted) — remove them so the \ + roster shrinks: {stale:?}" + ); + } +} diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index 70537b34d9e..ee3a7bd57ca 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -3150,7 +3150,7 @@ pub fn emit_lib_rs_from_files( __result }); let hand_maintained_mods = if has_compiler_tests.clone() { - "\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;".to_string() + "\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;".to_string() } else { "".to_string() }; diff --git a/src/v1/stage0/src/v1_compiler_infer_method.rs b/src/v1/stage0/src/v1_compiler_infer_method.rs index 0eed3e7cf49..5a18d6c296e 100644 --- a/src/v1/stage0/src/v1_compiler_infer_method.rs +++ b/src/v1/stage0/src/v1_compiler_infer_method.rs @@ -311,6 +311,38 @@ pub fn builtin_function_registry() -> Rc>> { int_type(), ); let m = v1_rt::rc_map_insert(m.clone(), "doc_graph_doc_count".to_string(), int_type()); + let m = v1_rt::rc_map_insert(m.clone(), "inert_carrier_count".to_string(), int_type()); + let m = v1_rt::rc_map_insert( + m.clone(), + "inert_carrier_unrostered_count".to_string(), + int_type(), + ); + let m = v1_rt::rc_map_insert( + m.clone(), + "inert_carrier_stale_roster_count".to_string(), + int_type(), + ); + let m = v1_rt::rc_map_insert( + m.clone(), + "inert_carrier_declared_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(), + "non_fold_residue_unrostered_count".to_string(), + int_type(), + ); + let m = v1_rt::rc_map_insert( + m.clone(), + "non_fold_residue_stale_roster_count".to_string(), + int_type(), + ); + let m = v1_rt::rc_map_insert( + m.clone(), + "non_fold_residue_coproduct_universe_count".to_string(), + int_type(), + ); let m = v1_rt::rc_map_insert( m.clone(), "transport_script_literal_violation_count_for_path".to_string(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 9b3355d7468..3733aab4473 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -5252,6 +5252,32 @@ fn eval_builtin( crate::doc_reachability_project::doc_graph_doc_count(), ))), + "inert_carrier_count" => Ok(Some(Value::Int( + crate::inert_carrier_project::inert_carrier_count(), + ))), + "inert_carrier_unrostered_count" => Ok(Some(Value::Int( + crate::inert_carrier_project::inert_carrier_unrostered_count(), + ))), + "inert_carrier_stale_roster_count" => Ok(Some(Value::Int( + crate::inert_carrier_project::inert_carrier_stale_roster_count(), + ))), + "inert_carrier_declared_count" => Ok(Some(Value::Int( + crate::inert_carrier_project::inert_carrier_declared_count(), + ))), + + "non_fold_residue_count" => Ok(Some(Value::Int( + crate::non_fold_residue_project::non_fold_residue_count(), + ))), + "non_fold_residue_unrostered_count" => Ok(Some(Value::Int( + crate::non_fold_residue_project::non_fold_residue_unrostered_count(), + ))), + "non_fold_residue_stale_roster_count" => Ok(Some(Value::Int( + crate::non_fold_residue_project::non_fold_residue_stale_roster_count(), + ))), + "non_fold_residue_coproduct_universe_count" => Ok(Some(Value::Int( + crate::non_fold_residue_project::non_fold_residue_coproduct_universe_count(), + ))), + _ => Ok(None), } } diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag new file mode 100644 index 00000000000..be9a3483b0b --- /dev/null +++ b/src/v2/lens/inert_carrier.dag @@ -0,0 +1,32 @@ +module v2.lens.inert_carrier + +import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.std.logic { Bool } + +fn inert_carrier_clean_holds() -> Bool { + inert_carrier_unrostered_count() == 0 && inert_carrier_stale_roster_count() == 0 +} + +fn inert_carrier_live_count() -> Int { + inert_carrier_count() +} + +fn inert_carrier_live_unrostered_count() -> Int { + inert_carrier_unrostered_count() +} + +fn inert_carrier_live_stale_roster_count() -> Int { + inert_carrier_stale_roster_count() +} + +fn inert_carrier_live_declared_count() -> Int { + inert_carrier_declared_count() +} + +data construction_justification: ConstructionJustification = ConstructionJustification { + class: WallAfterGrounding { + grounding_authority: "the realization loop wiring each carrier's real consumer, plus gunbc#5364 (.dag compile-graph / BindsTo enumeration) folding the host token census into a pure .dag reachability reader", + dissolve_on: "the exception roster reaches 0 as each self-tested carrier's consumer lands; the lens then walls any new self-tested-but-unconsumed carrier outright" + }, + rationale: "Inertness (self-tested + zero real consumer) is decidable, but cannot be made unwritable by construction -- modeling a carrier ahead of its consumer is the project's deliberate model-first discipline, so the bad state is legitimately writable in transit. So this is the unstructurable residue a lens is for: a fail-closed wall against a named, shrinking roster, not a construction." +} diff --git a/src/v2/lens/inert_carrier_test.dag b/src/v2/lens/inert_carrier_test.dag new file mode 100644 index 00000000000..2ab32b5b2eb --- /dev/null +++ b/src/v2/lens/inert_carrier_test.dag @@ -0,0 +1,15 @@ +module v2.test.lens_inert_carrier.inert_carrier_test + +import v2.std.logic { Bool } +import v2.lens.inert_carrier { + inert_carrier_clean_holds, + inert_carrier_live_declared_count +} + +test fn inert_carrier_no_unrostered_or_stale() -> Bool { + return inert_carrier_clean_holds() +} + +test fn inert_carrier_universe_is_nonempty() -> Bool { + return inert_carrier_live_declared_count() > 0 +} diff --git a/src/v2/lens/non_fold_residue.dag b/src/v2/lens/non_fold_residue.dag new file mode 100644 index 00000000000..5382211942d --- /dev/null +++ b/src/v2/lens/non_fold_residue.dag @@ -0,0 +1,32 @@ +module v2.lens.non_fold_residue + +import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import v2.std.logic { Bool } + +fn non_fold_residue_clean_holds() -> Bool { + non_fold_residue_unrostered_count() == 0 && non_fold_residue_stale_roster_count() == 0 +} + +fn non_fold_residue_live_count() -> Int { + non_fold_residue_count() +} + +fn non_fold_residue_live_unrostered_count() -> Int { + non_fold_residue_unrostered_count() +} + +fn non_fold_residue_live_stale_roster_count() -> Int { + non_fold_residue_stale_roster_count() +} + +fn non_fold_residue_live_coproduct_universe_count() -> Int { + non_fold_residue_coproduct_universe_count() +} + +data construction_justification: ConstructionJustification = ConstructionJustification { + class: WallAfterGrounding { + grounding_authority: "exhaustiveness-by-default in the typechecker (the DESIGN §4 CoproductExhaustiveness direction) making a wildcard over a closed coproduct unwritable, plus gunbc#5364 (.dag compile-graph access) folding the host match scan into a pure .dag Node-tree reader", + dissolve_on: "the un-migrated-modeling subset of the roster shrinks to 0 as each hand-rolled match migrates to a total fold; the named irreducible kernels (eq / lattice join+meet / collapse algebraic totals, whose off-diagonal IS the residue) remain by DESIGN section 6; the lens walls any NEW wildcard over a closed coproduct outright" + }, + rationale: "A wildcard over a closed coproduct is decidable residue, but cannot be banned by construction yet -- exhaustiveness-by-default is a load-bearing typechecker change, and a wildcard is legitimate over open/primitive domains. So this is the unstructurable residue a lens is for: a fail-closed wall against a named, shrinking roster, not a construction." +} diff --git a/src/v2/lens/non_fold_residue_test.dag b/src/v2/lens/non_fold_residue_test.dag new file mode 100644 index 00000000000..be648280339 --- /dev/null +++ b/src/v2/lens/non_fold_residue_test.dag @@ -0,0 +1,15 @@ +module v2.test.lens_non_fold_residue.non_fold_residue_test + +import v2.std.logic { Bool } +import v2.lens.non_fold_residue { + non_fold_residue_clean_holds, + non_fold_residue_live_coproduct_universe_count +} + +test fn non_fold_residue_no_unrostered_or_stale() -> Bool { + return non_fold_residue_clean_holds() +} + +test fn non_fold_residue_coproduct_universe_is_nonempty() -> Bool { + return non_fold_residue_live_coproduct_universe_count() > 0 +}