From 031082c2b0112cd6a306917e1030400630f2355c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 04:23:17 +0000 Subject: [PATCH 1/5] WIP: Promote-or-delete every inert lens and de-vacuum thin gates: each lens u --- src/v1/stage0/src/cli_run.rs | 108 ++++++++++++++++++++++++++++++++++- 1 file changed, 106 insertions(+), 2 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index e1a36381ee2..e6bee1a1e3e 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,98 @@ 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, From 9805baa36e39586f24886de492ca708f637247f5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 04:33:53 +0000 Subject: [PATCH 2/5] WIP: Promote-or-delete every inert lens and de-vacuum thin gates: each lens u --- src/v1/stage0/src/cli_run.rs | 102 ++++++++++++++++++ .../workflow/lens_effect_family_eval_test.dag | 34 ++++++ ...af_model_verification_family_eval_test.dag | 68 ++++++++++++ ...ag => lens_ownership_family_eval_test.dag} | 6 +- .../lens_subsumption_family_eval_test.dag | 45 ++++++++ ...ens_unused_parameters_family_eval_test.dag | 26 +++++ 6 files changed, 279 insertions(+), 2 deletions(-) create mode 100644 src/v2/workflow/lens_effect_family_eval_test.dag create mode 100644 src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag rename src/v2/workflow/{lens_ownership_family_eval.dag => lens_ownership_family_eval_test.dag} (85%) create mode 100644 src/v2/workflow/lens_subsumption_family_eval_test.dag create mode 100644 src/v2/workflow/lens_unused_parameters_family_eval_test.dag diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index e6bee1a1e3e..934a28489ed 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -3899,3 +3899,105 @@ 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..b4210fad8df --- /dev/null +++ b/src/v2/workflow/lens_effect_family_eval_test.dag @@ -0,0 +1,34 @@ +// 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.compiler.eval { + TestClaimRun, + test_claim_run_verdict +} +import v2.std.logic { Bool } +import v2.std.node { Node } +import v2.std.runtime { RuntimeValue } +import v2.std.verdict { Pass } +import v2.test.lens_effect.effect_depends_on { + effect_depends_on_claim_passes, + run_lens_effect_depends_on_runtime_verdict +} + +fn lens_effect_run_passes(run: TestClaimRun) -> Bool { + match test_claim_run_verdict(run: run) { + Pass => true + _ => false + } +} + +// Fail-closed: the structural lens classification holds AND the runtime claim run Passes. +fn lens_effect_family_gate() -> Bool { + effect_depends_on_claim_passes + && lens_effect_run_passes(run: run_lens_effect_depends_on_runtime_verdict) +} + +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..d937e80bc38 --- /dev/null +++ b/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag @@ -0,0 +1,68 @@ +// 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 +} + +// A fixture pair is verification-ready iff its happy probe is expected to ACCEPT and its +// falsification probe is expected to REJECT — i.e. the two probes discriminate. +fn leaf_model_pair_discriminates(pair: LeafModelFixturePair) -> Bool { + match pair.expected_happy_verdict { + TargetCompileAccepted => + match pair.falsification.expected_verdict { + TargetCompileRejected { diagnostic_code: _ } => true + TargetCompileAccepted => false + } + TargetCompileRejected { diagnostic_code: _ } => false + } +} + +fn leaf_model_rust_fixture_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 pairs = leaf_model_rust_fixture_pairs() + if is_empty(xs: pairs) { + false + } else { + fold_list( + xs: pairs, + empty: true, + cons: fn(acc, pair) { acc && leaf_model_pair_discriminates(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_test.dag similarity index 85% rename from src/v2/workflow/lens_ownership_family_eval.dag rename to src/v2/workflow/lens_ownership_family_eval_test.dag index 88267998ee8..799dc8efff9 100644 --- a/src/v2/workflow/lens_ownership_family_eval.dag +++ b/src/v2/workflow/lens_ownership_family_eval_test.dag @@ -1,4 +1,6 @@ -// Status: source-shape receipt; host CI can pin this file until generated item-registry compile-time lens replaces explicit family rosters. +// Status: discovered fail-closed family eval — routes the ownership lens subject roster through +// run_test_claim; the `test data` witness is auto-enrolled by the floor (DESIGN.md §6 inert-lens +// hygiene: every lens is a discovered fail-closed witness or deleted). Empty roster => false. module v2.test.workflow.lens_ownership_family_eval @@ -84,6 +86,6 @@ fn lens_ownership_family_gate(report: LensOwnershipFamilyEvalReport) -> Bool { } -data witness_lens_ownership_family_gate_closed: Bool = lens_ownership_family_gate( +test 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_subsumption_family_eval_test.dag b/src/v2/workflow/lens_subsumption_family_eval_test.dag new file mode 100644 index 00000000000..9bca8641640 --- /dev/null +++ b/src/v2/workflow/lens_subsumption_family_eval_test.dag @@ -0,0 +1,45 @@ +// Status: discovered fail-closed family eval for the subsumption (dissolution) lens (DESIGN.md §6 +// inert-lens hygiene: every lens is a discovered fail-closed witness or deleted). Routes the +// canonical DissolutionSubsumption MechanicalReverification receipt through run_test_claim and +// asserts BOTH the row-receipt run and the reverifies run Pass AND the mechanical verdict is +// Verified. Any non-Pass / non-Verified => RED (the lens carrier no longer reverifies). + +module v2.test.workflow.lens_subsumption_family_eval + +import v2.compiler.eval { + TestClaimRun, + test_claim_run_verdict +} +import v2.std.logic { Bool } +import v2.std.node { Node } +import v2.std.runtime { RuntimeValue } +import v2.std.verdict { Pass } +import v2.test.manual.dissolution_subsumption_reverification { + MechanicalReverificationVerdict, + Verified, + run_rust_language_model_emit_mechanical_reverification_claim, + run_rust_language_model_emit_subsumption_reverifies, + verdict_rust_language_model_emit_subsumption +} + +fn lens_subsumption_run_passes(run: TestClaimRun) -> Bool { + match test_claim_run_verdict(run: run) { + Pass => true + _ => false + } +} + +fn lens_subsumption_verdict_is_verified(v: MechanicalReverificationVerdict) -> Bool { + match v { + Verified => true + _ => false + } +} + +fn lens_subsumption_family_gate() -> Bool { + lens_subsumption_run_passes(run: run_rust_language_model_emit_mechanical_reverification_claim) + && lens_subsumption_run_passes(run: run_rust_language_model_emit_subsumption_reverifies) + && lens_subsumption_verdict_is_verified(v: verdict_rust_language_model_emit_subsumption) +} + +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..e6446483c05 --- /dev/null +++ b/src/v2/workflow/lens_unused_parameters_family_eval_test.dag @@ -0,0 +1,26 @@ +// 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() From 1ddc85442c912b16095741e1eae03ba45db30ce6 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 04:44:23 +0000 Subject: [PATCH 3/5] WIP: Promote-or-delete every inert lens and de-vacuum thin gates: each lens u --- .../lens_subsumption_family_eval_test.dag | 64 +++++++++---------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/src/v2/workflow/lens_subsumption_family_eval_test.dag b/src/v2/workflow/lens_subsumption_family_eval_test.dag index 9bca8641640..ccd8087aa4e 100644 --- a/src/v2/workflow/lens_subsumption_family_eval_test.dag +++ b/src/v2/workflow/lens_subsumption_family_eval_test.dag @@ -1,45 +1,45 @@ -// Status: discovered fail-closed family eval for the subsumption (dissolution) lens (DESIGN.md §6 -// inert-lens hygiene: every lens is a discovered fail-closed witness or deleted). Routes the -// canonical DissolutionSubsumption MechanicalReverification receipt through run_test_claim and -// asserts BOTH the row-receipt run and the reverifies run Pass AND the mechanical verdict is -// Verified. Any non-Pass / non-Verified => RED (the lens carrier no longer reverifies). +// 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.compiler.eval { - TestClaimRun, - test_claim_run_verdict -} import v2.std.logic { Bool } -import v2.std.node { Node } -import v2.std.runtime { RuntimeValue } -import v2.std.verdict { Pass } -import v2.test.manual.dissolution_subsumption_reverification { - MechanicalReverificationVerdict, - Verified, - run_rust_language_model_emit_mechanical_reverification_claim, - run_rust_language_model_emit_subsumption_reverifies, - verdict_rust_language_model_emit_subsumption -} - -fn lens_subsumption_run_passes(run: TestClaimRun) -> Bool { - match test_claim_run_verdict(run: run) { - Pass => true - _ => false - } +import v2.lens.subsumption { + DiffId, + DissolutionSubsumption, + MechanicalReverification, + ProducerStageDerivation, + affected_set_irt1_subsumption, + rust_language_model_emit_subsumption } -fn lens_subsumption_verdict_is_verified(v: MechanicalReverificationVerdict) -> Bool { - match v { - Verified => true - _ => false +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 { - lens_subsumption_run_passes(run: run_rust_language_model_emit_mechanical_reverification_claim) - && lens_subsumption_run_passes(run: run_rust_language_model_emit_subsumption_reverifies) - && lens_subsumption_verdict_is_verified(v: verdict_rust_language_model_emit_subsumption) + 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() From 3767c1b6cda1a95f754e62322b3929653d77acf8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 04:54:52 +0000 Subject: [PATCH 4/5] WIP: Promote-or-delete every inert lens and de-vacuum thin gates: each lens u --- .../workflow/lens_effect_family_eval_test.dag | 22 +---- ...af_model_verification_family_eval_test.dag | 58 +++++++++---- .../lens_ownership_family_eval_test.dag | 87 ++----------------- ...ens_unused_parameters_family_eval_test.dag | 3 +- 4 files changed, 55 insertions(+), 115 deletions(-) diff --git a/src/v2/workflow/lens_effect_family_eval_test.dag b/src/v2/workflow/lens_effect_family_eval_test.dag index b4210fad8df..ba313c82a00 100644 --- a/src/v2/workflow/lens_effect_family_eval_test.dag +++ b/src/v2/workflow/lens_effect_family_eval_test.dag @@ -5,30 +5,16 @@ module v2.test.workflow.lens_effect_family_eval -import v2.compiler.eval { - TestClaimRun, - test_claim_run_verdict -} import v2.std.logic { Bool } -import v2.std.node { Node } -import v2.std.runtime { RuntimeValue } -import v2.std.verdict { Pass } import v2.test.lens_effect.effect_depends_on { - effect_depends_on_claim_passes, - run_lens_effect_depends_on_runtime_verdict -} - -fn lens_effect_run_passes(run: TestClaimRun) -> Bool { - match test_claim_run_verdict(run: run) { - Pass => true - _ => false - } + effect_depends_on_claim_passes } -// Fail-closed: the structural lens classification holds AND the runtime claim run 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 - && lens_effect_run_passes(run: run_lens_effect_depends_on_runtime_verdict) } 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 index d937e80bc38..bd5cf51dc02 100644 --- a/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag +++ b/src/v2/workflow/lens_leaf_model_verification_family_eval_test.dag @@ -28,20 +28,43 @@ import v2.std.leaf_model_verification { TargetCompileRejected } -// A fixture pair is verification-ready iff its happy probe is expected to ACCEPT and its -// falsification probe is expected to REJECT — i.e. the two probes discriminate. -fn leaf_model_pair_discriminates(pair: LeafModelFixturePair) -> Bool { +fn leaf_model_pair_happy_accepts(pair: LeafModelFixturePair) -> Bool { match pair.expected_happy_verdict { - TargetCompileAccepted => - match pair.falsification.expected_verdict { - TargetCompileRejected { diagnostic_code: _ } => true - TargetCompileAccepted => false - } + TargetCompileAccepted => true TargetCompileRejected { diagnostic_code: _ } => false } } -fn leaf_model_rust_fixture_pairs() -> List { +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(), @@ -52,17 +75,22 @@ fn leaf_model_rust_fixture_pairs() -> List { } fn lens_leaf_model_verification_family_gate() -> Bool { - let pairs = leaf_model_rust_fixture_pairs() - if is_empty(xs: pairs) { + 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: pairs, + 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_discriminates(pair: pair) } + 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() +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_test.dag b/src/v2/workflow/lens_ownership_family_eval_test.dag index 799dc8efff9..260337cd609 100644 --- a/src/v2/workflow/lens_ownership_family_eval_test.dag +++ b/src/v2/workflow/lens_ownership_family_eval_test.dag @@ -1,91 +1,18 @@ -// Status: discovered fail-closed family eval — routes the ownership lens subject roster through -// run_test_claim; the `test data` witness is auto-enrolled by the floor (DESIGN.md §6 inert-lens -// hygiene: every lens is a discovered fail-closed witness or deleted). Empty roster => false. +// 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.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 { +fn lens_ownership_family_gate() -> 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) - } -} - - -test data witness_lens_ownership_family_gate_closed: Bool = lens_ownership_family_gate( - report: run_lens_ownership_family_eval() -) +test data witness_lens_ownership_family_gate_closed: Bool = lens_ownership_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 index e6446483c05..67e54007b21 100644 --- a/src/v2/workflow/lens_unused_parameters_family_eval_test.dag +++ b/src/v2/workflow/lens_unused_parameters_family_eval_test.dag @@ -22,5 +22,4 @@ fn lens_unused_parameters_family_gate() -> Bool { && unused_parameters_rollup_claim_passes } -test data witness_lens_unused_parameters_family_gate_closed: Bool = - lens_unused_parameters_family_gate() +test data witness_lens_unused_parameters_family_gate_closed: Bool = lens_unused_parameters_family_gate() From c26d5b87506b0f5a27211b185735de8d2c1d85bb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 05:02:07 +0000 Subject: [PATCH 5/5] fmt: inert-lens backstop --- src/v1/stage0/src/cli_run.rs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 934a28489ed..e43d533b6c7 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -2565,8 +2565,10 @@ fn inert_lens_modules( 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(); + 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()) { @@ -3927,12 +3929,16 @@ mod inert_lens_hygiene_tests { #[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")); + 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.test.lens_effect.effect_depends_on" + )); assert!(!is_top_level_lens_module("v2.std.algebra")); assert!(!is_top_level_lens_module("v2.lens.")); } @@ -3944,7 +3950,10 @@ mod inert_lens_hygiene_tests { 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()); + 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).