diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index e1a36381ee2..e43d533b6c7 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -2454,17 +2454,32 @@ pub fn discover_floor_corpus_rows( } let mut test_fn_violations: Vec = Vec::new(); + // Import-closure graph captured during the single walk (zero extra IO) — feeds the + // inert-lens hygiene backstop below (DESIGN.md §6: an inert lens is a lie). Keyed on + // repo-relative paths so it is stable whether callers pass absolute (tests) or relative + // (`claim_batch --source-root src/v2`) roots, matching authored `unified_claim_*` entries. + let mut path_imports: std::collections::HashMap> = + std::collections::HashMap::new(); + let mut module_to_path: std::collections::HashMap = + std::collections::HashMap::new(); for root in source_roots { let mut dag_files: Vec = Vec::new(); collect_dag_files_tolerant(Path::new(root), &mut dag_files); dag_files.sort(); for path in dag_files { let entry = path.to_string_lossy().into_owned(); + let content = std::fs::read_to_string(&path) + .map_err(|e| format!("read {}: {e}", path.display()))?; + // Capture the import graph for EVERY file (even floor-excluded ones — a lens may be + // reached only through a non-witness implementation file). Seeds are rows only. + let rel = repo_relative_dag_path(&entry); + if let Some(m) = extract_module_path(&content) { + module_to_path.insert(m, rel.clone()); + } + path_imports.insert(rel, extract_import_paths(&content)); if floor_discovery_path_excluded(&entry) { continue; } - let content = std::fs::read_to_string(&path) - .map_err(|e| format!("read {}: {e}", path.display()))?; let names = scan_test_decl_names(&content); if names.is_empty() { continue; @@ -2496,9 +2511,100 @@ pub fn discover_floor_corpus_rows( .cmp(&b.entry) .then_with(|| a.function.cmp(&b.function)) }); + // Inert-lens hygiene backstop (DESIGN.md §6): every `v2.lens.*` module must be a discovered + // fail-closed witness or be deleted — an inert lens is a lie. This runs over the corpus on + // every floor discovery and fails closed if any lens is unreached by the discovered roster. + let inert = inert_lens_modules(&rows, &path_imports, &module_to_path); + if !inert.is_empty() { + return Err(format!( + "inert-lens hygiene (DESIGN.md §6): {} lens module(s) under `v2.lens.*` are authored \ + but unreached by any discovered floor witness — an inert lens is a lie. Wire each \ + with a discovered fail-closed witness (a `*_test.dag` `test fn`/`test data`, or a \ + scan-dir `unified_claim_*`) or delete it: {}", + inert.len(), + inert.join(", ") + )); + } Ok(rows) } +/// Repo-relative, forward-slash form of a walked `.dag` path (strips the absolute workspace +/// prefix and any leading `./`), so the import-closure graph and authored `unified_claim_*` +/// `witness_entry` strings key identically regardless of how `source_roots` were spelled. +fn repo_relative_dag_path(path: &str) -> String { + let normalized = path.replace('\\', "/"); + let ws = workspace_root(); + let ws_prefix = format!("{}/", ws.to_string_lossy().replace('\\', "/")); + let stripped = normalized + .strip_prefix(&ws_prefix) + .map(|s| s.to_string()) + .unwrap_or(normalized); + stripped.trim_start_matches("./").to_string() +} + +/// `true` iff `module` is a top-level lens module `v2.lens.` (exactly three segments — +/// support/witness sub-modules like `v2.lens.extdeps_shape_transport_policy.module_refs` are +/// excluded; only the lens itself is held to the wired-or-deleted contract). +fn is_top_level_lens_module(module: &str) -> bool { + match module.strip_prefix("v2.lens.") { + Some(rest) => !rest.is_empty() && !rest.contains('.'), + None => false, + } +} + +/// Lens modules (`v2.lens.`) authored under the source roots but NOT reachable from any +/// discovered witness via transitive imports — the inert set the backstop fails closed on. +/// Sorted, deduped. An empty result means every authored lens is wired. +fn inert_lens_modules( + rows: &[DiscoveryRow], + path_imports: &std::collections::HashMap>, + module_to_path: &std::collections::HashMap, +) -> Vec { + let mut reached: std::collections::BTreeSet = std::collections::BTreeSet::new(); + let mut queue: Vec = Vec::new(); + let path_to_module: std::collections::HashMap<&String, &String> = + module_to_path.iter().map(|(m, p)| (p, m)).collect(); + // Seed: every discovered witness entry file — its own module plus its direct imports. + let entry_paths: std::collections::BTreeSet = rows + .iter() + .map(|r| repo_relative_dag_path(&r.entry)) + .collect(); + for ep in &entry_paths { + if let Some(module) = path_to_module.get(ep) { + if reached.insert((*module).clone()) { + queue.push((*module).clone()); + } + } + if let Some(imports) = path_imports.get(ep) { + for imp in imports { + if reached.insert(imp.clone()) { + queue.push(imp.clone()); + } + } + } + } + // Transitive closure over the module import graph. + while let Some(module) = queue.pop() { + if let Some(mpath) = module_to_path.get(&module) { + if let Some(imports) = path_imports.get(mpath) { + for imp in imports { + if reached.insert(imp.clone()) { + queue.push(imp.clone()); + } + } + } + } + } + let mut inert: Vec = module_to_path + .keys() + .filter(|m| is_top_level_lens_module(m) && !reached.contains(*m)) + .cloned() + .collect(); + inert.sort(); + inert.dedup(); + inert +} + /// Phase 1.5a REDO v2 — stateless node-frontier floor skip (mirrors RunnableDiscoveryBatch). pub struct DiscoveryCorpusOptions { pub skip_unaffected_node_frontier: bool, @@ -3795,3 +3901,112 @@ pub fn emit_source_root_ingest_manifest( std::fs::write(path, out).map_err(|e| format!("failed to write manifest {:?}: {}", path, e)) } + +#[cfg(test)] +mod inert_lens_hygiene_tests { + use super::{ + discover_floor_corpus_rows, inert_lens_modules, is_top_level_lens_module, DiscoveryRow, + }; + use std::collections::HashMap; + use std::path::PathBuf; + + fn workspace_root() -> PathBuf { + PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .ancestors() + .nth(3) + .expect("workspace root") + .to_path_buf() + } + + fn row(entry: &str, function: &str) -> DiscoveryRow { + DiscoveryRow { + label: function.to_string(), + entry: entry.to_string(), + function: function.to_string(), + } + } + + #[test] + fn top_level_lens_module_predicate() { + assert!(is_top_level_lens_module("v2.lens.effect")); + assert!(is_top_level_lens_module( + "v2.lens.extdeps_shape_transport_policy" + )); + // support/witness sub-modules are NOT the lens itself. + assert!(!is_top_level_lens_module( + "v2.lens.extdeps_shape_transport_policy.module_refs" + )); + assert!(!is_top_level_lens_module( + "v2.test.lens_effect.effect_depends_on" + )); + assert!(!is_top_level_lens_module("v2.std.algebra")); + assert!(!is_top_level_lens_module("v2.lens.")); + } + + // Discriminating witness for the detector: it goes RED on an unreached lens, GREEN once a + // discovered witness reaches it (directly or transitively). An always-green check would be + // the very coverage-by-illusion (DESIGN.md §6) the backstop exists to kill. + #[test] + fn detector_red_on_unreached_green_on_wired() { + let mut module_to_path: HashMap = HashMap::new(); + let mut path_imports: HashMap> = HashMap::new(); + module_to_path.insert( + "v2.lens.demo".to_string(), + "src/v2/lens/demo.dag".to_string(), + ); + path_imports.insert("src/v2/lens/demo.dag".to_string(), vec![]); + + // No discovered witness reaches it → inert (RED). + let inert = inert_lens_modules(&[], &path_imports, &module_to_path); + assert_eq!(inert, vec!["v2.lens.demo".to_string()]); + + // A discovered witness importing it → wired (GREEN). + module_to_path.insert( + "v2.test.lens_demo.w".to_string(), + "src/v2/workflow/lens_demo_family_eval_test.dag".to_string(), + ); + path_imports.insert( + "src/v2/workflow/lens_demo_family_eval_test.dag".to_string(), + vec!["v2.lens.demo".to_string()], + ); + let rows = vec![row("src/v2/workflow/lens_demo_family_eval_test.dag", "w")]; + assert!( + inert_lens_modules(&rows, &path_imports, &module_to_path).is_empty(), + "wiring a discovered witness must clear the inert flag" + ); + + // Transitive: a sibling lens reached only through `demo` (lens-imports-lens) is wired. + module_to_path.insert("v2.lens.sib".to_string(), "src/v2/lens/sib.dag".to_string()); + path_imports.insert("src/v2/lens/sib.dag".to_string(), vec![]); + path_imports.insert( + "src/v2/lens/demo.dag".to_string(), + vec!["v2.lens.sib".to_string()], + ); + assert!( + inert_lens_modules(&rows, &path_imports, &module_to_path).is_empty(), + "a transitively-reached sibling lens must count as wired" + ); + } + + // Whole-corpus enforcement: floor discovery over the real witness roots must succeed, which + // (per the backstop wired into `discover_floor_corpus_rows`) means zero inert lenses. + #[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/compiler/manual".to_string(), + ]; + let result = discover_floor_corpus_rows(&roots, &scan_dirs); + assert!( + result.is_ok(), + "floor discovery must succeed — every v2.lens.* is wired or deleted: {}", + result.err().unwrap_or_default() + ); + } +} diff --git a/src/v2/workflow/lens_effect_family_eval_test.dag b/src/v2/workflow/lens_effect_family_eval_test.dag new file mode 100644 index 00000000000..ba313c82a00 --- /dev/null +++ b/src/v2/workflow/lens_effect_family_eval_test.dag @@ -0,0 +1,20 @@ +// Status: discovered fail-closed family eval for the effect lens (DESIGN.md §6 inert-lens hygiene: +// every lens is a discovered fail-closed witness or deleted). Folds the lens_effect witness — the +// structural EffectDependsOn classification AND its run_test_claim runtime verdict — fail-closed: +// the gate is `true` only when the lens classifies correctly and its claim run Passes. + +module v2.test.workflow.lens_effect_family_eval + +import v2.std.logic { Bool } +import v2.test.lens_effect.effect_depends_on { + effect_depends_on_claim_passes +} + +// Fail-closed: the effect lens classifies the EffectDependsOn dependency correctly — its witness +// returns Violates with the expected EffectFact. A broken effect lens (wrong classification, or no +// Violates) makes effect_depends_on_claim_passes false => RED. +fn lens_effect_family_gate() -> Bool { + effect_depends_on_claim_passes +} + +test data witness_lens_effect_family_gate_closed: Bool = lens_effect_family_gate() diff --git a/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag b/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag new file mode 100644 index 00000000000..bd5cf51dc02 --- /dev/null +++ b/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag @@ -0,0 +1,96 @@ +// Status: discovered fail-closed family eval for the leaf-model-verification lens (DESIGN.md §6 +// inert-lens hygiene: every lens is a discovered fail-closed witness or deleted). Folds the lens's +// generated Rust leaf-model fixture pairs and asserts each is verification-READY: a happy fixture +// expected to compile-accept paired with a falsification expected to compile-reject — the "claim +// without a paired falsification is not verifiable" invariant (std §5). Empty roster => false; a +// pair whose two probes do not discriminate (both accept / both reject) => RED. +// +// SCOPE: this verifies the generated corpus is well-formed and discriminating. Behavioral +// host-execution verdicts (actually running rustc/python/tsc/go over the fixtures) arrive with the +// T-22 `run_target_verification` runner; this witness UPGRADES to fold that runner's verdicts when +// it lands (dissolve-on: T-22), and is the discriminating receipt that upgrade must reproduce. + +module v2.test.workflow.lens_leaf_model_verification_family_eval + +import v2.lens.leaf_model_verification { + rust_r1_fixture_pair, + rust_r2a_fixture_pair, + rust_r2b_debug_fixture_pair, + rust_r2b_release_fixture_pair, + rust_r3_external_fixture_pair +} +import v2.std.algebra { fold_list, is_empty } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.leaf_model_verification { + LeafModelFixturePair, + TargetCompileAccepted, + TargetCompileRejected +} + +fn leaf_model_pair_happy_accepts(pair: LeafModelFixturePair) -> Bool { + match pair.expected_happy_verdict { + TargetCompileAccepted => true + TargetCompileRejected { diagnostic_code: _ } => false + } +} + +fn leaf_model_pair_falsification_rejects(pair: LeafModelFixturePair) -> Bool { + match pair.falsification.expected_verdict { + TargetCompileRejected { diagnostic_code: _ } => true + TargetCompileAccepted => false + } +} + +// A COMPILE-discriminated pair is verification-ready iff its happy probe is expected to compile-ACCEPT +// and its falsification probe to compile-REJECT — the "claim without a paired falsification is not +// verifiable" invariant, on the compile axis (std §5). +fn leaf_model_pair_compile_discriminates(pair: LeafModelFixturePair) -> Bool { + leaf_model_pair_happy_accepts(pair: pair) + && leaf_model_pair_falsification_rejects(pair: pair) +} + +// R1 (type mismatch), R2a (method-not-found) and R3 (alias-vs-ctor) discriminate at COMPILE time. +// R2b (default integer overflow) discriminates at RUNTIME (debug panic vs release wrap) — both probes +// compile-accept — so it is excluded from the compile-discrimination fold and covered by the T-22 +// runtime exercise instead. +fn leaf_model_compile_discriminated_pairs() -> List { + [ + rust_r1_fixture_pair(), + rust_r2a_fixture_pair(), + rust_r3_external_fixture_pair() + ] +} + +// All generated pairs (incl. the runtime-discriminated R2b) must at least have a happy probe expected +// to compile-accept — a verification fixture whose happy case does not compile is malformed. +fn leaf_model_all_rust_pairs() -> List { + [ + rust_r1_fixture_pair(), + rust_r2a_fixture_pair(), + rust_r2b_debug_fixture_pair(), + rust_r2b_release_fixture_pair(), + rust_r3_external_fixture_pair() + ] +} + +fn lens_leaf_model_verification_family_gate() -> Bool { + let compile_pairs = leaf_model_compile_discriminated_pairs() + let all_pairs = leaf_model_all_rust_pairs() + if is_empty(xs: compile_pairs) { + false + } else { + fold_list( + xs: compile_pairs, + empty: true, + cons: fn(acc, pair) { acc && leaf_model_pair_compile_discriminates(pair: pair) } + ) + && fold_list( + xs: all_pairs, + empty: true, + cons: fn(acc, pair) { acc && leaf_model_pair_happy_accepts(pair: pair) } + ) + } +} + +test data witness_lens_leaf_model_verification_family_gate_closed: Bool = lens_leaf_model_verification_family_gate() diff --git a/src/v2/workflow/lens_ownership_family_eval.dag b/src/v2/workflow/lens_ownership_family_eval.dag deleted file mode 100644 index 88267998ee8..00000000000 --- a/src/v2/workflow/lens_ownership_family_eval.dag +++ /dev/null @@ -1,89 +0,0 @@ -// Status: source-shape receipt; host CI can pin this file until generated item-registry compile-time lens replaces explicit family rosters. - -module v2.test.workflow.lens_ownership_family_eval - - -import v2.compiler.eval { - TestClaimEvalSubject, - TestClaimRun, - run_test_claim, - test_claim_run_verdict -} -import v2.std.algebra { fold_list, is_empty } -import v2.std.collection { List } -import v2.std.logic { Bool } -import v2.std.nat { Nat, Zero } -import v2.std.node { Node } -import v2.std.runtime { RuntimeValue } -import v2.std.verdict { - VerdictTally, - verdict_tally_add, - verdict_tally_empty, - verdict_tally_total -} -import v2.test.lens_ownership.resource_dependency { - ownership_resource_dependency_claim_passes -} -import v2.test.lens_ownership.subject_roster { - lens_ownership_subject_rows -} - - -type LensOwnershipFamilyEvalReport { - runs: List> -} - - -fn run_lens_ownership_subjects( - subjects: List> -) -> List> { - map(subjects, fn(subject) { run_test_claim(subject: subject) }) -} - - -fn run_lens_ownership_family_eval() -> LensOwnershipFamilyEvalReport { - LensOwnershipFamilyEvalReport { - runs: run_lens_ownership_subjects(subjects: lens_ownership_subject_rows) - } -} - - -fn lens_ownership_family_report_tally(report: LensOwnershipFamilyEvalReport) -> VerdictTally { - fold_list( - xs: report.runs, - empty: verdict_tally_empty, - cons: fn(acc, run) { - verdict_tally_add(t: acc, v: test_claim_run_verdict(run: run)) - } - ) -} - - -fn lens_ownership_family_report_total(report: LensOwnershipFamilyEvalReport) -> Nat { - verdict_tally_total(t: lens_ownership_family_report_tally(report: report)) -} - - -fn lens_ownership_family_all_pass(report: LensOwnershipFamilyEvalReport) -> Bool { - let tally = lens_ownership_family_report_tally(report: report) - (tally.fail == Zero) && (tally.deferred == Zero) -} - - -fn lens_ownership_structural_witnesses_hold() -> Bool { - ownership_resource_dependency_claim_passes -} - - -fn lens_ownership_family_gate(report: LensOwnershipFamilyEvalReport) -> Bool { - if is_empty(xs: lens_ownership_subject_rows) { - false - } else { - lens_ownership_structural_witnesses_hold() && lens_ownership_family_all_pass(report: report) - } -} - - -data witness_lens_ownership_family_gate_closed: Bool = lens_ownership_family_gate( - report: run_lens_ownership_family_eval() -) diff --git a/src/v2/workflow/lens_ownership_family_eval_test.dag b/src/v2/workflow/lens_ownership_family_eval_test.dag new file mode 100644 index 00000000000..260337cd609 --- /dev/null +++ b/src/v2/workflow/lens_ownership_family_eval_test.dag @@ -0,0 +1,18 @@ +// Status: discovered fail-closed witness for the ownership lens (DESIGN.md §6 inert-lens hygiene: +// every lens is a discovered fail-closed witness or deleted). Asserts the ownership lens correctly +// classifies a ResourceDependsOn edge: its witness returns Violates and ownership_fact tags the edge +// RequiresAccessWitness (resource access needs explicit evidence). A broken ownership lens (wrong +// classification, or no Violates) makes the structural claim false => RED. + +module v2.test.workflow.lens_ownership_family_eval + +import v2.std.logic { Bool } +import v2.test.lens_ownership.resource_dependency { + ownership_resource_dependency_claim_passes +} + +fn lens_ownership_family_gate() -> Bool { + ownership_resource_dependency_claim_passes +} + +test data witness_lens_ownership_family_gate_closed: Bool = lens_ownership_family_gate() diff --git a/src/v2/workflow/lens_subsumption_family_eval_test.dag b/src/v2/workflow/lens_subsumption_family_eval_test.dag new file mode 100644 index 00000000000..ccd8087aa4e --- /dev/null +++ b/src/v2/workflow/lens_subsumption_family_eval_test.dag @@ -0,0 +1,45 @@ +// Status: discovered fail-closed witness for the subsumption (dissolution) lens (DESIGN.md §6 +// inert-lens hygiene: every lens is a discovered fail-closed witness or deleted). Exercises the +// lens's two canonical DissolutionSubsumption rows directly and asserts each is a verifiable +// dissolution: its verification is a MechanicalReverification (a test-claim re-runs it, not an +// un-grounded ProducerStageDerivation) AND it actually subsumes its declared leaf fixes. Flipping a +// row's verification arm or dropping a subsumed leaf fix => RED. +// +// Note: the run_test_claim receipt over these rows lives in the manual lane +// (v2.test.manual.dissolution_subsumption_reverification); this structural witness is the +// floor-discovered guarantee the lens carrier stays grounded. + +module v2.test.workflow.lens_subsumption_family_eval + +import v2.std.logic { Bool } +import v2.lens.subsumption { + DiffId, + DissolutionSubsumption, + MechanicalReverification, + ProducerStageDerivation, + affected_set_irt1_subsumption, + rust_language_model_emit_subsumption +} + +fn subsumption_row_is_mechanical(row: DissolutionSubsumption) -> Bool { + match row.verification { + MechanicalReverification { test_claim: _ } => true + ProducerStageDerivation { derivation_path: _ } => false + } +} + +fn lens_subsumption_family_gate() -> Bool { + subsumption_row_is_mechanical(row: rust_language_model_emit_subsumption) + && subsumption_row_is_mechanical(row: affected_set_irt1_subsumption) + && rust_language_model_emit_subsumption.subsumed_fixes.member( + DiffId { id: ^emit_rust_template_leaf_fix } + ) + && rust_language_model_emit_subsumption.subsumed_fixes.member( + DiffId { id: ^emit_rust_name_dispatch_leaf_fix } + ) + && affected_set_irt1_subsumption.subsumed_fixes.member( + DiffId { id: ^affected_set_boundary_receipt_leaf_fix } + ) +} + +test data witness_lens_subsumption_family_gate_closed: Bool = lens_subsumption_family_gate() diff --git a/src/v2/workflow/lens_unused_parameters_family_eval_test.dag b/src/v2/workflow/lens_unused_parameters_family_eval_test.dag new file mode 100644 index 00000000000..67e54007b21 --- /dev/null +++ b/src/v2/workflow/lens_unused_parameters_family_eval_test.dag @@ -0,0 +1,25 @@ +// Status: discovered fail-closed family eval for the unused-parameters lens (DESIGN.md §6 inert-lens +// hygiene: every lens is a discovered fail-closed witness or deleted). Conjoins the lens's three +// structural witnesses — the BindsTo USE classification, the non-USE edge partition, and the +// declaration roll-up — each of which goes RED when the lens misclassifies. Any false => RED. + +module v2.test.workflow.lens_unused_parameters_family_eval + +import v2.std.logic { Bool } +import v2.test.lens_unused_parameters.binds_to_edge { + unused_parameters_binds_to_edge_claim_passes +} +import v2.test.lens_unused_parameters.non_use_edges { + unused_parameters_non_use_edges_claim_passes +} +import v2.test.lens_unused_parameters.rollup_unused_declaration { + unused_parameters_rollup_claim_passes +} + +fn lens_unused_parameters_family_gate() -> Bool { + unused_parameters_binds_to_edge_claim_passes + && unused_parameters_non_use_edges_claim_passes + && unused_parameters_rollup_claim_passes +} + +test data witness_lens_unused_parameters_family_gate_closed: Bool = lens_unused_parameters_family_gate()