Skip to content
9 changes: 9 additions & 0 deletions dsl/test/claim/inert_lens_hygiene_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module test.claim.inert_lens_hygiene_witness

test fn inert_lens_hygiene_has_no_unreached_modules() -> Bool {
return inert_lens_unreached_module_count() == 0
}

test fn inert_lens_hygiene_universe_is_nonempty() -> Bool {
return inert_lens_top_level_module_count() > 0
}
2 changes: 2 additions & 0 deletions src/v1/04_method.dag
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,8 @@ fn builtin_function_registry() -> Map<String, Node> {
let m = map_insert(m, "inert_carrier_unrostered_count", int_type)
let m = map_insert(m, "inert_carrier_stale_roster_count", int_type)
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)
Expand Down
102 changes: 92 additions & 10 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2724,12 +2724,19 @@ pub fn discover_floor_corpus_rows_scoped(
)
}

fn discover_floor_corpus_rows_inner(
struct FloorLensHygieneGraph {
rows: Vec<DiscoveryRow>,
path_imports: std::collections::HashMap<String, Vec<String>>,
module_to_path: std::collections::HashMap<String, String>,
lens_with_justification: std::collections::BTreeSet<String>,
}

fn build_floor_lens_hygiene_graph(
source_roots: &[String],
scan_dirs: &[String],
exclude_substrings: &[String],
discovery_scope_dirs: &[String],
) -> Result<Vec<DiscoveryRow>, String> {
) -> Result<FloorLensHygieneGraph, String> {
let excludes: Vec<String> = exclude_substrings.to_vec();
let mut rows: Vec<DiscoveryRow> = Vec::new();
let mut seen: std::collections::BTreeSet<(String, String)> = std::collections::BTreeSet::new();
Expand Down Expand Up @@ -2843,6 +2850,72 @@ fn discover_floor_corpus_rows_inner(
.cmp(&b.entry)
.then_with(|| a.function.cmp(&b.function))
});
Ok(FloorLensHygieneGraph {
rows,
path_imports,
module_to_path,
lens_with_justification,
})
}

fn default_floor_lens_hygiene_excludes() -> Vec<String> {
FLOOR_DISCOVERY_EXCLUDES
.iter()
.map(|s| s.to_string())
.collect()
}

/// 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 {
match build_floor_lens_hygiene_graph(
&crate::module_path_index::default_source_roots(),
&crate::module_path_index::witness_discovery_scan_dirs(),
&default_floor_lens_hygiene_excludes(),
&[],
) {
Ok(graph) => {
inert_lens_modules(&graph.rows, &graph.path_imports, &graph.module_to_path).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 {
match build_floor_lens_hygiene_graph(
&crate::module_path_index::default_source_roots(),
&crate::module_path_index::witness_discovery_scan_dirs(),
&default_floor_lens_hygiene_excludes(),
&[],
) {
Ok(graph) => graph
.module_to_path
.keys()
.filter(|m| is_top_level_lens_module(m))
.count() as i64,
Err(_) => -1,
}
}

fn discover_floor_corpus_rows_inner(
source_roots: &[String],
scan_dirs: &[String],
exclude_substrings: &[String],
discovery_scope_dirs: &[String],
) -> Result<Vec<DiscoveryRow>, String> {
let graph = build_floor_lens_hygiene_graph(
source_roots,
scan_dirs,
exclude_substrings,
discovery_scope_dirs,
)?;
let FloorLensHygieneGraph {
rows,
path_imports,
module_to_path,
lens_with_justification,
} = graph;
let inert = inert_lens_modules(&rows, &path_imports, &module_to_path);
if !inert.is_empty() {
return Err(format!(
Expand Down Expand Up @@ -4627,18 +4700,27 @@ mod inert_lens_hygiene_tests {
);
}

#[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 = vec![
ws.join("dsl").to_string_lossy().into_owned(),
ws.join("src/v2").to_string_lossy().into_owned(),
];
let scan_dirs = vec![
"dsl/test/claim".to_string(),
"src/v2/test/claim/manual".to_string(),
];
let roots = crate::module_path_index::default_source_roots();
let scan_dirs = crate::module_path_index::witness_discovery_scan_dirs();
let excludes: Vec<String> = FLOOR_DISCOVERY_EXCLUDES
.iter()
.map(|s| s.to_string())
Expand Down
109 changes: 80 additions & 29 deletions src/v1/stage0/src/module_path_index.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,33 @@ pub fn workspace_root() -> std::path::PathBuf {
// authority, the same direction gunbc#5364 takes the residue scan.)
const CI_LAYER_ROOTS_AUTHORITY_REL: &str = "dsl/gunbc/ci_layer_roots.dag";
const WITNESS_LAYER_ROOTS_DATA_NAME: &str = "witness_layer_roots";
const WITNESS_DISCOVERY_SCAN_DIRS_DATA_NAME: &str = "witness_discovery_scan_dirs";

/// Project the `witness_layer_roots` `List<String>` literal out of the ci_layer_roots authority's
/// SOURCE TEXT via the real front-end (`tokenize` + `parse`) — no second hand-rolled scanner. Pure
/// (text in, roots out) so a synthetic authority carrying non-default roots can drive it: a reader
/// that ignored its input and returned a hardcoded `["dsl", "src/v2"]` (the reverted shape) fails that
/// control — the by-construction discrimination (DESIGN §5). Fail-closed: a parse error, a missing data
/// def, a non-string-list body, or an empty list is a loud panic, never a silent fallback that would
/// re-open the drift.
pub(crate) fn witness_layer_roots_from_source(content: &str) -> Vec<String> {
fn ci_layer_roots_authority_content() -> &'static str {
static CONTENT: OnceLock<String> = OnceLock::new();
CONTENT
.get_or_init(|| {
let path = workspace_root().join(CI_LAYER_ROOTS_AUTHORITY_REL);
std::fs::read_to_string(&path).unwrap_or_else(|e| {
panic!(
"ci_layer_roots authority: failed to read {}: {e}",
path.display()
)
})
})
.as_str()
}

/// Project a `List<String>` data literal out of the ci_layer_roots authority's SOURCE TEXT via the
/// real front-end (`tokenize` + `parse`) — no second hand-rolled scanner. Pure (text in, list out) so
/// a synthetic authority carrying non-default values can drive it: a reader that ignored its input
/// and returned a hardcoded copy fails that control — the by-construction discrimination (DESIGN §5).
/// Fail-closed: a parse error, a missing data def, a non-string-list body, or an empty list is a loud
/// panic, never a silent fallback that would re-open the drift.
pub(crate) fn string_list_data_from_ci_layer_roots_source(
content: &str,
data_name: &str,
) -> Vec<String> {
use crate::v1_std_core::{ExprData, LiteralValue};

let filename = CI_LAYER_ROOTS_AUTHORITY_REL.to_string();
Expand All @@ -45,70 +63,80 @@ pub(crate) fn witness_layer_roots_from_source(content: &str) -> Vec<String> {
panic!("ci_layer_roots authority: {CI_LAYER_ROOTS_AUTHORITY_REL} parsed to no module")
});
for item in module.children.iter() {
if item.name != WITNESS_LAYER_ROOTS_DATA_NAME
if item.name != data_name
|| !crate::v1_compiler_emit_core_support::is_data_def_item(item.clone())
{
continue;
}
let body = item.body.as_ref().unwrap_or_else(|| {
panic!(
"ci_layer_roots authority: `data {WITNESS_LAYER_ROOTS_DATA_NAME}` in \
"ci_layer_roots authority: `data {data_name}` in \
{CI_LAYER_ROOTS_AUTHORITY_REL} has no value body"
)
});
if !matches!(body.expr_data.as_ref(), ExprData::ExprListLit) {
panic!(
"ci_layer_roots authority: `data {WITNESS_LAYER_ROOTS_DATA_NAME}` in \
"ci_layer_roots authority: `data {data_name}` in \
{CI_LAYER_ROOTS_AUTHORITY_REL} is not a `List<String>` literal"
);
}
let mut roots = Vec::new();
let mut values = Vec::new();
for el in body.children.iter() {
match el.expr_data.as_ref() {
ExprData::ExprLiteral { value } => match value.as_ref() {
LiteralValue::LitStr { value } => roots.push(value.clone()),
LiteralValue::LitStr { value } => values.push(value.clone()),
_ => panic!(
"ci_layer_roots authority: an element of `{WITNESS_LAYER_ROOTS_DATA_NAME}` in \
"ci_layer_roots authority: an element of `{data_name}` in \
{CI_LAYER_ROOTS_AUTHORITY_REL} is not a string literal"
),
},
_ => panic!(
"ci_layer_roots authority: an element of `{WITNESS_LAYER_ROOTS_DATA_NAME}` in \
"ci_layer_roots authority: an element of `{data_name}` in \
{CI_LAYER_ROOTS_AUTHORITY_REL} is not a literal"
),
}
}
if roots.is_empty() {
if values.is_empty() {
panic!(
"ci_layer_roots authority: `{WITNESS_LAYER_ROOTS_DATA_NAME}` in \
"ci_layer_roots authority: `{data_name}` in \
{CI_LAYER_ROOTS_AUTHORITY_REL} is empty (fail-closed: an empty witness corpus would \
vacuously pass every census wall)"
);
}
return roots;
return values;
}
panic!(
"ci_layer_roots authority: no `data {WITNESS_LAYER_ROOTS_DATA_NAME}` def in \
"ci_layer_roots authority: no `data {data_name}` def in \
{CI_LAYER_ROOTS_AUTHORITY_REL}"
)
}

/// Project the `witness_layer_roots` `List<String>` literal out of the ci_layer_roots authority.
pub(crate) fn witness_layer_roots_from_source(content: &str) -> Vec<String> {
string_list_data_from_ci_layer_roots_source(content, WITNESS_LAYER_ROOTS_DATA_NAME)
}

/// Project the `witness_discovery_scan_dirs` `List<String>` literal out of the ci_layer_roots
/// authority.
pub(crate) fn witness_discovery_scan_dirs_from_source(content: &str) -> Vec<String> {
string_list_data_from_ci_layer_roots_source(content, WITNESS_DISCOVERY_SCAN_DIRS_DATA_NAME)
}

/// The witness layer roots, read live from the single .dag authority and memoized (the authority is
/// fixed for a process's lifetime). Repo-relative roots (e.g. `dsl`, `src/v2`); consumers join them
/// onto `workspace_root()`. Every Rust census derives its corpus from HERE — see the module note.
pub(crate) fn witness_layer_roots() -> Vec<String> {
static ROOTS: OnceLock<Vec<String>> = OnceLock::new();
ROOTS
.get_or_init(|| {
let path = workspace_root().join(CI_LAYER_ROOTS_AUTHORITY_REL);
let content = std::fs::read_to_string(&path).unwrap_or_else(|e| {
panic!(
"ci_layer_roots authority: failed to read {}: {e}",
path.display()
)
});
witness_layer_roots_from_source(&content)
})
.get_or_init(|| witness_layer_roots_from_source(ci_layer_roots_authority_content()))
.clone()
}

/// Witness discovery scan dirs, read live from `gunbc.ci_layer_roots.witness_discovery_scan_dirs`.
pub(crate) fn witness_discovery_scan_dirs() -> Vec<String> {
static SCAN_DIRS: OnceLock<Vec<String>> = OnceLock::new();
SCAN_DIRS
.get_or_init(|| witness_discovery_scan_dirs_from_source(ci_layer_roots_authority_content()))
.clone()
}

Expand Down Expand Up @@ -217,4 +245,27 @@ mod tests {
]
);
}

#[test]
fn reader_follows_synthetic_authority_scan_dirs() {
let synthetic = "module gunbc.ci_layer_roots\n\n\
data witness_discovery_scan_dirs: List<String> = [\"scan/a\", \"scan/b\"]\n";
assert_eq!(
witness_discovery_scan_dirs_from_source(synthetic),
vec!["scan/a".to_string(), "scan/b".to_string()],
"the scan-dir reader must FOLLOW the authority, not a hardcoded copy"
);
}

#[test]
fn witness_discovery_scan_dirs_projects_live_authority_value() {
assert_eq!(
witness_discovery_scan_dirs(),
vec![
"dsl/test/claim".to_string(),
"src/v2/test/claim/manual".to_string(),
],
"live authority scan-dir value drifted"
);
}
}
10 changes: 10 additions & 0 deletions src/v1/stage0/src/v1_compiler_infer_method.rs
Original file line number Diff line number Diff line change
Expand Up @@ -330,6 +330,16 @@ pub fn builtin_function_registry() -> Rc<HashMap<String, Rc<Node>>> {
"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(),
Expand Down
7 changes: 7 additions & 0 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5770,6 +5770,13 @@ fn eval_builtin(
crate::inert_carrier_project::inert_carrier_declared_count(),
))),

"inert_lens_unreached_module_count" => Ok(Some(Value::Int(
crate::cli_run::inert_lens_unreached_module_count(),
))),
"inert_lens_top_level_module_count" => Ok(Some(Value::Int(
crate::cli_run::inert_lens_top_level_module_count(),
))),

"non_fold_residue_count" => Ok(Some(Value::Int(
crate::non_fold_residue_project::non_fold_residue_count(),
))),
Expand Down