From cb6e64ec189cc90838dbd7246ce8e46df0d0b4d7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 03:27:57 +0000 Subject: [PATCH 1/9] complexity foundation only: loop typing + measure-derived termination + claim-bin cwd fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reworked to drop the forked complexity machinery. The cost-shape lowering (dag_surface_lower_*) was a second, hand-rolled body producer running beside the compiler's own — a §3/§4 fork: it re-lowered the surface parse tree by hand (one if-arm per production), skipping resolve + normalize + body_producer, and produced a shape that matched neither the real inferred tree nor its own synthetic test subjects. It caught zero real quadratics and generated a cascade of point-fixes (per-form lowering lanes, a lexeme-recovery module, a GeneratedArtifact name collision, missing Branch-descent). All of it is backed out. The general body producer that would replace it — §4's "one grammar read in both directions" (row-driven ingest, the inverse of the row-driven emitter), which also subsumes the pre-existing MVP1 03_body_producer — is left as compiler work, not landed as a fork. Kept: the genuinely fork-free, DESIGN-clean behavioral changes. - 04_infer gains the Loop arm: an iteration-fold body is typed as a per-iteration transform (τ → τ under the measure); divergent and refinement-shaped bodies refuse with the located infer_loop_iteration_type_mismatch. - Measure-derived loop termination (loop_multiplicity over the cited measure_descent_fact_registry, lattice meet + lexicographic strict-dimension proof), grounded on the dag/std/termination.dag single authority. - claim_batch / claim_executor resolve relative path args against the process cwd and refuse (exit 2, located) on missing paths — closes the baked-root mixed-tree fail-open. Verified by execution against the merged base: 8 loop-multiplicity + 5 loop-infer witnesses PASS; roster-shape, generated-artifact drift, and enforcement-consistency + repo-wide-complexity meta-gates PASS. The two new loop tests are CI-enrolled so the kept behavior gates. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 33 +++ src/v1/stage0/src/bin/claim_batch.rs | 89 ++++++- src/v1/stage0/src/bin/claim_executor.rs | 18 +- src/v1/stage0/src/cli_run.rs | 149 ++++++++++++ src/v2/compiler/04_infer.dag | 190 +++++++++++++++ src/v2/std/cardinality.dag | 207 ++++++++++++++++- .../claim/execution/loop_round_trip_test.dag | 25 +- .../test/claim/loop_infer_iteration_test.dag | 143 ++++++++++++ .../claim/loop_multiplicity_measure_test.dag | 218 ++++++++++++++++++ 9 files changed, 1043 insertions(+), 29 deletions(-) create mode 100644 src/v2/test/claim/loop_infer_iteration_test.dag create mode 100644 src/v2/test/claim/loop_multiplicity_measure_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index d72ad32d077..38adfe0f28f 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -132,6 +132,39 @@ data commit_gate_roster: List = [ }, surfaces: [GithubActionsCiJob] }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/test/claim/loop_multiplicity_measure_test.dag", + check_fns: [ + "loop_strict_measure_infers_proven_termination", + "loop_perturbed_measure_is_refused", + "loop_lone_non_increasing_measure_is_refused", + "loop_lexicographic_measure_proves_with_strict_dimension", + "loop_unknown_dimension_poisons_lexicographic_measure", + "loop_missing_measure_is_refused", + "live_registry_proves_loop_measure", + "nested_unproven_loop_still_poisons_the_fold" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/test/claim/loop_infer_iteration_test.dag", + check_fns: [ + "loop_infer_invariant_body_accepts_with_carrier_type", + "loop_infer_divergent_body_is_refused", + "loop_infer_refinement_shaped_body_is_refused", + "loop_infer_unregistered_measure_is_refused", + "loop_infer_missing_measure_is_refused" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, CommitCheckEnrollment { check: CommitWitnessClaim { entry: "dag/test/claim/parse_test.dag", diff --git a/src/v1/stage0/src/bin/claim_batch.rs b/src/v1/stage0/src/bin/claim_batch.rs index 32198cf7526..1969b742c7a 100644 --- a/src/v1/stage0/src/bin/claim_batch.rs +++ b/src/v1/stage0/src/bin/claim_batch.rs @@ -151,6 +151,20 @@ fn require_value(args: &[String], idx: usize, flag: &str) -> Result Result { + let given = require_value(args, idx, flag)?; + match v1_compiler::cli_run::resolve_cli_path_arg("claim_batch", flag, &given) { + Ok(resolved) => Ok(resolved), + Err(msg) => { + eprintln!("{msg}"); + Err(ExitCode::from(2)) + } + } +} + struct EntryGroup { entry: String, functions: Vec, @@ -183,11 +197,11 @@ fn parse_args(args: &[String]) -> Result { match args[i].as_str() { "--source-root" => { i += 1; - source_roots.push(require_value(args, i, "--source-root")?); + source_roots.push(require_path_value(args, i, "--source-root")?); } "--entry" => { i += 1; - let entry = require_value(args, i, "--entry")?; + let entry = require_path_value(args, i, "--entry")?; entry_groups.push(EntryGroup { entry, functions: Vec::new(), @@ -223,7 +237,7 @@ fn parse_args(args: &[String]) -> Result { "--roster-from-discovery" => roster_from_discovery = true, "--scan-dir" => { i += 1; - scan_dirs.push(require_value(args, i, "--scan-dir")?); + scan_dirs.push(require_path_value(args, i, "--scan-dir")?); } "--notice-title" => { i += 1; @@ -639,6 +653,75 @@ fn main() -> ExitCode { } } +#[cfg(test)] +mod cli_path_resolution_wiring_tests { + use super::parse_args; + use v1_compiler::cli_run::workspace_root; + + fn args(v: &[&str]) -> Vec { + std::iter::once("claim_batch") + .chain(v.iter().copied()) + .map(str::to_string) + .collect() + } + + /// Absolute existing paths pass parse_args unchanged (resolution applied, no rewrite). + #[test] + fn absolute_existing_args_parse_and_survive_resolution() { + let ws = workspace_root(); + let root = ws.join("dag").to_string_lossy().into_owned(); + let entry = ws + .join("dag/test/claim/commit_workflow_witness_test.dag") + .to_string_lossy() + .into_owned(); + let parsed = parse_args(&args(&[ + "--source-root", + &root, + "--entry", + &entry, + "--function", + "commit_workflow_witnesses", + ])) + .unwrap_or_else(|_| panic!("absolute existing paths must parse")); + assert_eq!(parsed.source_roots, vec![root]); + assert_eq!(parsed.entry_groups.len(), 1); + assert_eq!(parsed.entry_groups[0].entry, entry); + } + + /// A nonexistent --source-root refuses at the CLI boundary (exit-code error), never + /// proceeding to a partial run. + #[test] + fn nonexistent_source_root_refuses_at_parse() { + assert!(parse_args(&args(&["--source-root", "/no/such/tree"])).is_err()); + } + + /// Relative args resolve against the PROCESS CWD, not the baked workspace root. + /// `cargo test` runs bin unit tests with cwd == the package dir (src/v1/stage0), + /// where `dag` does not exist — while it DOES exist under the baked workspace root. + /// parse_args must therefore agree with the cwd, whichever it is: refuse when + /// cwd/dag is absent (a baked-root fallback would accept), accept when present. + #[test] + fn relative_source_root_follows_process_cwd_not_baked_root() { + let cwd = std::env::current_dir().expect("test cwd"); + let cwd_has_dag = cwd.join("dag").is_dir(); + let result = parse_args(&args(&[ + "--source-root", + "dag", + "--entry", + "dag/test/claim/commit_workflow_witness_test.dag", + "--function", + "commit_workflow_witnesses", + ])); + assert_eq!( + result.is_ok(), + cwd_has_dag, + "relative --source-root must resolve against the process cwd {} (dag present: {cwd_has_dag}), never the baked workspace root {}", + cwd.display(), + workspace_root().display() + ); + } +} + #[cfg(test)] mod discovery_exclude_tests { use v1_compiler::cli_run::floor_discovery_path_excluded; diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index e2fd83baf0e..723926c2dcf 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -48,6 +48,20 @@ fn require_value(args: &[String], idx: usize, flag: &str) -> Result Result { + let given = require_value(args, idx, flag)?; + match v1_compiler::cli_run::resolve_cli_path_arg("claim_executor", flag, &given) { + Ok(resolved) => Ok(resolved), + Err(msg) => { + eprintln!("{msg}"); + Err(ExitCode::from(2)) + } + } +} + fn free_monoid_elems<'a>(value: &'a Value, ctx: &InterpContext) -> Result, String> { let mut out = Vec::new(); let mut cur = value; @@ -1701,11 +1715,11 @@ fn run() -> Result { } "--source-root" => { i += 1; - source_roots.push(require_value(&args, i, "--source-root")?); + source_roots.push(require_path_value(&args, i, "--source-root")?); } "--plan-entry" => { i += 1; - plan_entry = Some(require_value(&args, i, "--plan-entry")?); + plan_entry = Some(require_path_value(&args, i, "--plan-entry")?); } "--plan-function" => { i += 1; diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 07e9d420d01..bd6c342340e 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -175,6 +175,155 @@ pub fn workspace_root() -> PathBuf { .to_path_buf() } +/// CLI-boundary path resolution for the claim bins (`claim_batch` / `claim_executor`). +/// +/// `workspace_root()` above is baked from `env!("CARGO_MANIFEST_DIR")` at COMPILE time, +/// and part of the shared resolution pipeline (`pool_roots_abs`) anchors RELATIVE source +/// roots to that baked path while the module-content index reads them relative to the +/// process cwd. For the claim bins that meant a run from any other cwd (e.g. a git +/// worktree) silently mixed two trees — module contents from the cwd, import-graph facts +/// from the baked root — wrong answers with zero diagnostic (DESIGN §5 fail-open). +/// +/// The bins therefore resolve their path-valued arguments HERE, at the CLI boundary, +/// with standard CLI semantics: a relative path resolves against the PROCESS CWD, and a +/// resolved path that does not exist is a refusal naming the argument, the given value, +/// and the resolution base — never a fallback to the baked root, never a partial run. +/// When the cwd IS the baked workspace root, the relative spelling and the absolutized +/// spelling denote the same file for every downstream consumer (cwd-anchored reads and +/// baked-root-anchored reads agree), so the given spelling passes through unchanged and +/// the normal case (and CI) stays byte-identical. Any other cwd absolutizes, so the +/// baked-root anchoring in the shared pipeline can never re-route the read. +pub fn resolve_cli_path_arg(bin: &str, flag: &str, given: &str) -> Result { + if Path::new(given).is_absolute() { + return resolve_cli_path_arg_against(bin, flag, given, Path::new("/")); + } + let cwd = std::env::current_dir().map_err(|e| { + format!( + "{bin}: {flag} {given}: cannot resolve a relative CLI path — the process \ + working directory is unavailable: {e}" + ) + })?; + resolve_cli_path_arg_against(bin, flag, given, &cwd) +} + +/// Core of [`resolve_cli_path_arg`] with an explicit resolution base (testable without +/// mutating the process-global cwd). +fn resolve_cli_path_arg_against( + bin: &str, + flag: &str, + given: &str, + base: &Path, +) -> Result { + let given_path = Path::new(given); + if given_path.is_absolute() { + if !given_path.exists() { + return Err(format!( + "{bin}: {flag} {given}: absolute path does not exist; refusing (no \ + fallback to the compiled-in workspace root {})", + workspace_root().display() + )); + } + return Ok(given.to_string()); + } + let resolved = base.join(given_path); + if !resolved.exists() { + return Err(format!( + "{bin}: {flag} {given}: resolved against the process working directory {} \ + to {}, which does not exist; refusing — relative CLI paths resolve against \ + the process cwd, never the compiled-in workspace root {} — run from the \ + tree you meant or pass an absolute path", + base.display(), + resolved.display(), + workspace_root().display() + )); + } + let ws = workspace_root(); + if same_canonical_file(&base.to_string_lossy(), &ws.to_string_lossy()) { + return Ok(given.to_string()); + } + Ok(resolved.to_string_lossy().into_owned()) +} + +#[cfg(test)] +mod cli_path_arg_resolution_tests { + use super::{resolve_cli_path_arg_against, workspace_root}; + + fn fixture_base(tag: &str) -> std::path::PathBuf { + std::env::temp_dir().join(format!("gunbc-cli-path-arg-{tag}-{}", std::process::id())) + } + + /// (a) Relative arg with base == workspace root: byte-identical pass-through — + /// the exact string the bins forwarded before this boundary existed. + #[test] + fn relative_arg_at_workspace_root_passes_through_unchanged() { + let ws = workspace_root(); + let resolved = resolve_cli_path_arg_against("claim_batch", "--source-root", "dag", &ws) + .expect("`dag` exists under the workspace root"); + assert_eq!(resolved, "dag"); + } + + /// (b) Relative arg from a different cwd resolves against THAT cwd — the result is + /// the absolutized fixture path, never the bare relative spelling (which the shared + /// pipeline would re-anchor to the baked workspace root) and never a baked-root path. + #[test] + fn relative_arg_from_other_cwd_resolves_against_that_cwd() { + let base = fixture_base("other-cwd"); + std::fs::create_dir_all(base.join("dag")).expect("create fixture tree"); + std::fs::write(base.join("dag/mini.dag"), "module mini\n").expect("write fixture module"); + + let root = resolve_cli_path_arg_against("claim_batch", "--source-root", "dag", &base) + .expect("fixture tree exists under the fixture cwd"); + assert_eq!(root, base.join("dag").to_string_lossy()); + assert_ne!( + root, "dag", + "must absolutize away from the baked-root anchor" + ); + + let entry = resolve_cli_path_arg_against("claim_batch", "--entry", "dag/mini.dag", &base) + .expect("fixture entry exists under the fixture cwd"); + assert_eq!(entry, base.join("dag/mini.dag").to_string_lossy()); + + let _ = std::fs::remove_dir_all(&base); + } + + /// (c) Nonexistent relative path: refusal names the argument, the given value, and + /// the resolution base — and does NOT resolve against the baked workspace root even + /// though the path exists there (the discriminating red control for the fail-open). + #[test] + fn nonexistent_relative_arg_refuses_naming_flag_value_and_base() { + let base = fixture_base("refusal"); + std::fs::create_dir_all(&base).expect("create empty fixture cwd"); + // `dag` exists under the baked workspace root but NOT under `base`; a baked-root + // fallback would return Ok here — the refusal is the proof there is none. + let err = resolve_cli_path_arg_against("claim_batch", "--source-root", "dag", &base) + .expect_err("missing path must refuse, never fall back to the baked root"); + assert!(err.contains("claim_batch"), "names the binary: {err}"); + assert!(err.contains("--source-root"), "names the argument: {err}"); + assert!(err.contains("dag"), "names the given value: {err}"); + assert!( + err.contains(&base.display().to_string()), + "names the resolution base: {err}" + ); + let _ = std::fs::remove_dir_all(&base); + } + + /// Nonexistent absolute path refuses too — never proceeds partially. + #[test] + fn nonexistent_absolute_arg_refuses() { + let missing = fixture_base("absolute-missing").join("no/such/entry.dag"); + let missing_str = missing.to_string_lossy().into_owned(); + let err = resolve_cli_path_arg_against( + "claim_executor", + "--plan-entry", + &missing_str, + std::path::Path::new("/"), + ) + .expect_err("missing absolute path must refuse"); + assert!(err.contains("--plan-entry"), "names the argument: {err}"); + assert!(err.contains(&missing_str), "names the given value: {err}"); + } +} + /// Empty ingest-manifest placeholder excluded from the module index when a later /// source root carries the host-emitted manifest (source-root ingest / closure gates). const SOURCE_ROOT_INGEST_MANIFEST_STUB_REL: &str = diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index d8efca23cb3..b904296a4cd 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -47,6 +47,7 @@ import v2.std.node { Branch, ComputationNode, Edge, + Loop, Match, Node, NodeFold, @@ -55,6 +56,7 @@ import v2.std.node { TypeNode, all_edges_positional, fold_node, + loop_edge_contributes_to_iteration_fold, match_arm_body, match_arm_pattern, well_formed @@ -105,6 +107,7 @@ type InferGatherFoldAcc { pending: Diagnostics await_branch_row: Bool await_match_row: Bool + await_loop_row: Bool children_remaining: Int } @@ -155,6 +158,22 @@ fn infer_branch_arm_type_mismatch_diagnostic(node: Node) -> Diagnostic { } } +fn infer_loop_shape_invalid_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: ^infer_loop_shape_invalid, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn infer_loop_iteration_type_mismatch_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: ^infer_loop_iteration_type_mismatch, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + fn infer_match_shape_invalid_diagnostic(node: Node) -> Diagnostic { Diagnostic { reason: ^infer_match_shape_invalid, @@ -785,11 +804,105 @@ fn infer_match_bool( } } +data infer_loop_iteration_flag_c_note: String = "FLAG C (body-lowering design, operator-signed): the first cut types carrier-invariant loops only — every iteration-fold child must resolve to ONE carrier type τ, so the inferred tree states 'body : τ → τ, repeated under the measure'. A refinement-shaped loop (carrier narrows across iterations, e.g. Refined<τ> vs τ) lands in the located infer_loop_iteration_type_mismatch refusal by construction — refused, never silently fabricated as τ → τ. Dissolution trigger: the refinement-typed follow-on (monotone-narrowing carrier) replaces that refusal with a real refinement judgment." + +fn infer_loop_iteration_fold_child_targets(node: Node) -> List { + fold(node.children, init: [], f: fn(acc, e) { + if loop_edge_contributes_to_iteration_fold(parent: node, e: e) { + list_snoc_item(xs: acc, item: e.target) + } else { + acc + } + }) +} + +fn infer_loop_body_type_at(target: Node, entries: List) -> Outcome { + match lookup_inferred_facts_in_entries(entries: entries, key: target) { + Violates { diagnostic: d } => outcome_rejected(d) + Holds { value: facts } => + Accepted { + value: infer_branch_operand_resolved_type(node: target, facts: facts), + diagnostics: None + } + } +} + +fn infer_loop_fixpoint_carrier( + node: Node, + body_targets: List, + entries: List, +) -> Outcome { + match list_at_optional(xs: body_targets, index: 0) { + Absent => outcome_rejected(infer_loop_shape_invalid_diagnostic(node: node)) + Present { value: first_body } => + bind_outcome( + o: infer_loop_body_type_at(target: first_body, entries: entries), + f: fn(carrier) { + fold(body_targets, init: Accepted { value: carrier, diagnostics: None }, f: fn(acc, target) { + match acc { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: c, diagnostics: _ } => + match infer_loop_body_type_at(target: target, entries: entries) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: t, diagnostics: _ } => + if infer_branch_type_atoms_equal(a: c, b: t) { + acc + } else { + outcome_rejected(infer_loop_iteration_type_mismatch_diagnostic(node: target)) + } + } + } + }) + } + ) + } +} + +fn infer_loop_iteration( + node: Node, + partials: List, + entries: List, +) -> Outcome { + match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: _, diagnostics: cd } => + match infer_loop_fixpoint_carrier( + node: node, + body_targets: infer_loop_iteration_fold_child_targets(node: node), + entries: entries + ) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: carrier, diagnostics: ud } => + match infer_descent_witness_for_node(n: node) { + Violates { diagnostic: d } => + Rejected { diagnostics: diagnostics_singleton(d: d) } + Holds { value: descent_proof } => + bind_outcome( + o: inferred_facts_from_grounding( + grounding: infer_branch_canonical_grounding( + node: node, + unified_type: carrier + ), + descent: Holds { value: descent_proof } + ), + f: fn(facts) { + Accepted { + value: facts, + diagnostics: diagnostics_merge(outer: cd, inner: ud) + } + } + ) + } + } + } +} + fn infer_gather_fold_acc_failed( node: Node, pending: NonEmptyDiagnostics, await_branch_row: Bool, await_match_row: Bool, + await_loop_row: Bool, children_remaining: Int, ) -> InferGatherFoldAcc { InferGatherFoldAcc { @@ -799,6 +912,7 @@ fn infer_gather_fold_acc_failed( pending: Some { diagnostics: pending }, await_branch_row: await_branch_row, await_match_row: await_match_row, + await_loop_row: await_loop_row, children_remaining: children_remaining } } @@ -809,6 +923,7 @@ fn infer_gather_fold_acc_ok( pending: Diagnostics, await_branch_row: Bool, await_match_row: Bool, + await_loop_row: Bool, children_remaining: Int, ) -> InferGatherFoldAcc { InferGatherFoldAcc { @@ -818,6 +933,7 @@ fn infer_gather_fold_acc_ok( pending: pending, await_branch_row: await_branch_row, await_match_row: await_match_row, + await_loop_row: await_loop_row, children_remaining: children_remaining } } @@ -862,6 +978,7 @@ fn infer_gather_branch_row_on_entries( pending: rejected_with_pending(pending: pending, rejected: r), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: facts, diagnostics: d } => @@ -872,6 +989,7 @@ fn infer_gather_branch_row_on_entries( pending: rejected_with_pending(pending: pending, rejected: r), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: entry, diagnostics: ed } => @@ -884,6 +1002,7 @@ fn infer_gather_branch_row_on_entries( ), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) } @@ -903,6 +1022,7 @@ fn infer_gather_match_row_on_entries( pending: rejected_with_pending(pending: pending, rejected: r), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: facts, diagnostics: d } => @@ -913,6 +1033,7 @@ fn infer_gather_match_row_on_entries( pending: rejected_with_pending(pending: pending, rejected: r), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: entry, diagnostics: ed } => @@ -925,6 +1046,51 @@ fn infer_gather_match_row_on_entries( ), await_branch_row: false, await_match_row: false, + await_loop_row: false, + children_remaining: 0 + ) + } + } +} + +fn infer_gather_loop_row_on_entries( + node: Node, + entries: List, + pending: Diagnostics, + partials: List, +) -> InferGatherFoldAcc { + match infer_loop_iteration(node: node, partials: partials, entries: entries) { + Rejected { diagnostics: r } => + infer_gather_fold_acc_failed( + node: node, + pending: rejected_with_pending(pending: pending, rejected: r), + await_branch_row: false, + await_match_row: false, + await_loop_row: false, + children_remaining: 0 + ) + Accepted { value: facts, diagnostics: d } => + match admitted_inferred_facts_entry(node: node, facts: facts) { + Rejected { diagnostics: r } => + infer_gather_fold_acc_failed( + node: node, + pending: rejected_with_pending(pending: pending, rejected: r), + await_branch_row: false, + await_match_row: false, + await_loop_row: false, + children_remaining: 0 + ) + Accepted { value: entry, diagnostics: ed } => + infer_gather_fold_acc_ok( + node: node, + entries: list_snoc_item(xs: entries, item: entry), + pending: diagnostics_merge( + outer: diagnostics_merge(outer: pending, inner: d), + inner: ed + ), + await_branch_row: false, + await_match_row: false, + await_loop_row: false, children_remaining: 0 ) } @@ -940,6 +1106,7 @@ fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { pending: None, await_branch_row: true, await_match_row: false, + await_loop_row: false, children_remaining: length(xs: n.children) ) ComputationNode { behavior: Match } => @@ -949,6 +1116,17 @@ fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { pending: None, await_branch_row: false, await_match_row: true, + await_loop_row: false, + children_remaining: length(xs: n.children) + ) + ComputationNode { behavior: Loop } => + infer_gather_fold_acc_ok( + node: n, + entries: empty_inferred_facts_entry_list(), + pending: None, + await_branch_row: false, + await_match_row: false, + await_loop_row: true, children_remaining: length(xs: n.children) ) _ => @@ -959,6 +1137,7 @@ fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { pending: r, await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: facts, diagnostics: d } => @@ -969,6 +1148,7 @@ fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { pending: r, await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) Accepted { value: entry, diagnostics: ed } => @@ -978,6 +1158,7 @@ fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { pending: diagnostics_merge(outer: d, inner: ed), await_branch_row: false, await_match_row: false, + await_loop_row: false, children_remaining: 0 ) } @@ -1012,6 +1193,7 @@ fn infer_gather_fold_step( ), await_branch_row: acc.await_branch_row, await_match_row: acc.await_match_row, + await_loop_row: acc.await_loop_row, children_remaining: acc.children_remaining ) } else { @@ -1032,6 +1214,13 @@ fn infer_gather_fold_step( pending: merged_pending, partials: partials ) + } else if acc.await_loop_row && children_remaining == 0 { + infer_gather_loop_row_on_entries( + node: acc.node, + entries: merged_entries, + pending: merged_pending, + partials: partials + ) } else { infer_gather_fold_acc_ok( node: acc.node, @@ -1039,6 +1228,7 @@ fn infer_gather_fold_step( pending: merged_pending, await_branch_row: acc.await_branch_row, await_match_row: acc.await_match_row, + await_loop_row: acc.await_loop_row, children_remaining: children_remaining ) } diff --git a/src/v2/std/cardinality.dag b/src/v2/std/cardinality.dag index e3f736d1974..bd9d188f5ea 100644 --- a/src/v2/std/cardinality.dag +++ b/src/v2/std/cardinality.dag @@ -1,6 +1,14 @@ module v2.std.cardinality -import v2.std.collection { List } +import std.algebra { Cons, Empty } +import std.termination { + DescentEvidence, + Strict, + NonIncreasing, + DescentUnknown, + descent_evidence_lattice_meet +} +import v2.std.collection { Absent, List, Optional, Present } import v2.std.diagnostic { Diagnostic, ExternalContractUnknown, @@ -223,10 +231,205 @@ fn behavior_multiplicity(b: Behavior) -> Multiplicity { } } +data measure_descent_registry_note: String = "Measure descent facts ground the loop termination derivation on the single DescentEvidence authority (std.termination — operator standing rule 2026-07-08: dag/std wins v2↔dag forks; body-lowering design Stage 2/T1). A measure Atom carries descent evidence only via a cited registry row; an unregistered symbol is DescentUnknown — the lattice bottom — so an unproven measure refuses, never fabricates. Same grounded symbol→fact registry pattern as v2.std.algebra.copied_port_fact_registry." + +type MeasureDescentFact { + measure: Symbol + evidence: DescentEvidence + citation: String +} + +data measure_descent_fact_structural_node_size: MeasureDescentFact = { + measure: ^cardinality_structural_node_size, + evidence: Strict, + citation: "v2.std.node.fold_node structural recursion: every child is a strict subtree of its parent — the dimension structural_node_size_termination_proof already names" +} + +data measure_descent_fact_dag_loop_measure: MeasureDescentFact = { + measure: ^dag_loop_measure_sym, + evidence: Strict, + citation: "loop-body producer's declared loop bound (v2.extdeps.languages.dag.dag_loop_measure_node); grounds the exact TerminationProof that loop_round_trip_test and loop_eval_by_execution_test previously hand-fabricated per test site" +} + +data measure_descent_fact_fold_iteration: MeasureDescentFact = { + measure: ^dag_surface_fold_iteration_measure, + evidence: Strict, + citation: "fold iteration over a finite collection descends by construction (std.termination DescentSource.FoldIteration: each step consumes one element of the folded list); the surface cost-shape lowering stamps this measure on every fold-family call it lowers to Loop (v2.extdeps.languages.dag)" +} + +data measure_descent_fact_registry: List = [ + measure_descent_fact_structural_node_size, + measure_descent_fact_dag_loop_measure, + measure_descent_fact_fold_iteration +] + +fn measure_descent_some(e: DescentEvidence) -> Optional { + Present { value: e } +} + +fn measure_descent_fact_for(registry: List, s: Symbol) -> Optional { + fold(registry, init: Absent, f: fn(acc, row) { + match acc { + Present { value: _ } => acc + Absent => + if row.measure == s { + measure_descent_some(e: row.evidence) + } else { + Absent + } + } + }) +} + +fn measure_descent_evidence_for_symbol(registry: List, s: Symbol) -> DescentEvidence { + match measure_descent_fact_for(registry: registry, s: s) { + Present { value: e } => e + Absent => DescentUnknown + } +} + +type MeasureDimensionEvidence { + dimension: RankingDimension + evidence: DescentEvidence +} + +fn measure_dimension_unknown_rows() -> List { + [ + MeasureDimensionEvidence { + dimension: RankingDimension { measured: ^cardinality_measure_shape_unknown }, + evidence: DescentUnknown + } + ] +} + +fn measure_dimension_rows(registry: List, measure: Node) -> List { + match measure.kind { + TypeNode { connective: c } => + match c { + Atom { identity: s } => + [ + MeasureDimensionEvidence { + dimension: RankingDimension { measured: s }, + evidence: measure_descent_evidence_for_symbol(registry: registry, s: s) + } + ] + Conj => + fold(measure.children, init: Empty, f: fn(acc, e) { + fold(measure_dimension_rows(registry: registry, measure: e.target), init: acc, f: fn(acc2, row) { + Cons { head: row, tail: acc2 } + }) + }) + Disj => measure_dimension_unknown_rows() + Arrow => measure_dimension_unknown_rows() + Cardinality => measure_dimension_unknown_rows() + Instantiation => measure_dimension_unknown_rows() + } + ComputationNode { behavior: _ } => measure_dimension_unknown_rows() + } +} + +fn dimension_rows_meet(rows: List) -> DescentEvidence { + fold(rows, init: Strict, f: fn(acc, row) { + descent_evidence_lattice_meet(a: acc, b: row.evidence) + }) +} + +fn dimension_row_is_strict(row: MeasureDimensionEvidence) -> Bool { + match row.evidence { + Strict => true + NonIncreasing => false + DescentUnknown => false + } +} + +fn ranking_dimension_some(d: RankingDimension) -> Optional { + Present { value: d } +} + +fn first_strict_dimension(rows: List) -> Optional { + fold(rows, init: Absent, f: fn(acc, row) { + match acc { + Present { value: _ } => acc + Absent => + if dimension_row_is_strict(row: row) { + ranking_dimension_some(d: row.dimension) + } else { + Absent + } + } + }) +} + +type LexicographicSplit { + strict_taken: Bool + non_increasing: List +} + +fn non_strict_dimensions_after_first(rows: List) -> List { + let split = fold(rows, init: LexicographicSplit { strict_taken: false, non_increasing: Empty }, f: fn(acc, row) { + if dimension_row_is_strict(row: row) && !acc.strict_taken { + LexicographicSplit { strict_taken: true, non_increasing: acc.non_increasing } + } else { + LexicographicSplit { + strict_taken: acc.strict_taken, + non_increasing: Cons { head: row.dimension, tail: acc.non_increasing } + } + } + }) + split.non_increasing +} + +fn lexicographic_multiplicity(rows: List) -> Multiplicity { + match first_strict_dimension(rows: rows) { + Absent => RequiresTerminationProof + Present { value: strict_dim } => + ProvenTermination { + proof: TerminationProof { + non_increasing: non_strict_dimensions_after_first(rows: rows), + strict: strict_dim + } + } + } +} + +fn loop_multiplicity_from_rows(rows: List) -> Multiplicity { + if count(rows) == 0 { + RequiresTerminationProof + } else { + match dimension_rows_meet(rows: rows) { + DescentUnknown => RequiresTerminationProof + NonIncreasing => lexicographic_multiplicity(rows: rows) + Strict => lexicographic_multiplicity(rows: rows) + } + } +} + +fn loop_multiplicity_with(registry: List, n: Node) -> Multiplicity { + match loop_measure_node(n: n) { + Violates { diagnostic: _ } => RequiresTerminationProof + Holds { value: measure } => + loop_multiplicity_from_rows(rows: measure_dimension_rows(registry: registry, measure: measure)) + } +} + +fn loop_multiplicity(n: Node) -> Multiplicity { + loop_multiplicity_with(registry: measure_descent_fact_registry, n: n) +} + +data loop_multiplicity_node_aware_note: String = "FLAG B (body-lowering design, operator-signed): Loop multiplicity is decided node-aware here while the other behaviors stay tag-only in behavior_multiplicity — a real distinction, not inconsistency: only Loop's termination depends on a node-level edge (the ^loop_bound_edge measure), which the Behavior tag structurally cannot carry. behavior_multiplicity(Loop) stays RequiresTerminationProof as the honest measure-less projection." + fn node_multiplicity(n: Node) -> Multiplicity { match n.kind { TypeNode { connective: c } => connective_multiplicity(c: c) - ComputationNode { behavior: b } => behavior_multiplicity(b: b) + ComputationNode { behavior: b } => + match b { + Value => behavior_multiplicity(b: b) + Transform => behavior_multiplicity(b: b) + Branch => behavior_multiplicity(b: b) + Loop => loop_multiplicity(n: n) + Bind => behavior_multiplicity(b: b) + Match => behavior_multiplicity(b: b) + } } } diff --git a/src/v2/test/claim/execution/loop_round_trip_test.dag b/src/v2/test/claim/execution/loop_round_trip_test.dag index 2cc8ec91c87..789ed6327a1 100644 --- a/src/v2/test/claim/execution/loop_round_trip_test.dag +++ b/src/v2/test/claim/execution/loop_round_trip_test.dag @@ -19,7 +19,6 @@ import v2.extdeps.languages.dag { } import v2.test.lens_common.infer_fixture { claim_inferred_facts_witness } import v2.std.cardinality { - RankingDimension, TerminationProof, termination_proof_witness_for_node } @@ -40,7 +39,7 @@ import v2.std.diagnostic { node_locus } import v2.std.logic { Bool } -import v2.std.node { ComputationNode, Node } +import v2.std.node { Node } import v2.std.compilers.target_model { TargetModel } import v2.std.witness { Holds, StructuralPropertyWitness, Violates, Witness } import v2.std.verification { @@ -136,28 +135,10 @@ fn loop_canonical_grounding_for(node: Node) -> Witness { } } -fn loop_termination_proof() -> TerminationProof { - TerminationProof { - non_increasing: [], - strict: RankingDimension { measured: ^dag_loop_measure_sym } - } -} - -fn loop_round_trip_node_is_loop(node: Node) -> Bool { - match node.kind { - ComputationNode { behavior: Loop } => true - _ => false - } -} +data loop_descent_fabrication_dissolved_note: String = "The former loop_descent_witness_for hand-fabricated Holds { TerminationProof { strict: ^dag_loop_measure_sym } } for every loop node because the tag-only multiplicity path unconditionally refused loops. Body-lowering Stage 2 (measure_descent_fact_registry, v2.std.cardinality) derives that exact proof from the measure, so the fabrication is deleted and this test consumes the real derivation." fn loop_descent_witness_for(node: Node) -> Witness { - if node == dag_fixture_emitted_loop_fn - || node == dag_loop_body_fixture - || loop_round_trip_node_is_loop(node: node) { - Holds { value: loop_termination_proof() } - } else { - termination_proof_witness_for_node(n: node) - } + termination_proof_witness_for_node(n: node) } fn loop_round_trip_inferred_facts_for(node: Node) -> Witness { diff --git a/src/v2/test/claim/loop_infer_iteration_test.dag b/src/v2/test/claim/loop_infer_iteration_test.dag new file mode 100644 index 00000000000..057940b354f --- /dev/null +++ b/src/v2/test/claim/loop_infer_iteration_test.dag @@ -0,0 +1,143 @@ +module v2.test.claim.loop_infer_iteration + +import v2.compiler.infer { + infer, + infer_branch_type_atoms_equal, + inferred_facts_resolved_type, + inferred_facts_witness_for_node, + InferredTree +} +import v2.compiler.resolve { ResolvedTree } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.logic { Bool } +import v2.std.node { + Atom, + ComputationNode, + Edge, + Loop, + Named, + Node, + Positional, + Symbol, + SyntheticOccurrence, + TypeNode +} +import v2.std.witness { Holds, Violates } + +data loop_infer_refinement_proxy_note: String = "FLAG C witness (body-lowering design, operator-signed): the refinement-shaped case stands in for a carrier that narrows across iterations — its second stage resolves to a different type than the first stage's carrier, exactly the class a Refined<τ>-narrowing loop lands in under atom-equality unification. It must be REFUSED with the located infer_loop_iteration_type_mismatch, never silently fabricated as τ → τ. Dissolves with the refinement-typed follow-on named in infer_loop_iteration_flag_c_note." + +fn loop_infer_atom(s: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: s } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn loop_infer_int_binding_type_node() -> Node { + loop_infer_atom(s: ^dag_binding_type_int) +} + +fn loop_infer_two_stage_loop_node(first: Node, second: Node, measure: Node) -> Node { + Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: first }, + Edge { label: Positional, target: second }, + Edge { label: Named { name: ^loop_bound_edge }, target: measure } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn loop_infer_one_stage_loop_node(stage: Node, measure: Node) -> Node { + Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: stage }, + Edge { label: Named { name: ^loop_bound_edge }, target: measure } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn loop_infer_registered_measure() -> Node { + loop_infer_atom(s: ^dag_loop_measure_sym) +} + +fn loop_infer_run(root: Node) -> Outcome { + infer(tree: root) +} + +fn loop_infer_loop_type_is_int(tree: InferredTree, body: Node) -> Bool { + match inferred_facts_witness_for_node(tree: tree, node: body) { + Holds { value: facts } => + infer_branch_type_atoms_equal( + a: inferred_facts_resolved_type(facts: facts), + b: loop_infer_int_binding_type_node() + ) + Violates { diagnostic: _ } => false + } +} + +test fn loop_infer_invariant_body_accepts_with_carrier_type() -> Bool { + let body = loop_infer_two_stage_loop_node( + first: loop_infer_atom(s: ^dag_pick_lit_one), + second: loop_infer_atom(s: ^dag_pick_lit_two), + measure: loop_infer_registered_measure() + ) + match loop_infer_run(root: body) { + Accepted { value: inferred, diagnostics: _ } => + loop_infer_loop_type_is_int(tree: inferred, body: body) + Rejected { diagnostics: _ } => false + } +} + +test fn loop_infer_divergent_body_is_refused() -> Bool { + let body = loop_infer_two_stage_loop_node( + first: loop_infer_atom(s: ^dag_pick_lit_one), + second: loop_infer_atom(s: ^dag_token_kw_true), + measure: loop_infer_registered_measure() + ) + match loop_infer_run(root: body) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn loop_infer_refinement_shaped_body_is_refused() -> Bool { + let body = loop_infer_two_stage_loop_node( + first: loop_infer_atom(s: ^dag_pick_lit_one), + second: loop_infer_atom(s: ^loop_infer_refined_int_carrier), + measure: loop_infer_registered_measure() + ) + match loop_infer_run(root: body) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn loop_infer_unregistered_measure_is_refused() -> Bool { + let body = loop_infer_one_stage_loop_node( + stage: loop_infer_atom(s: ^dag_pick_lit_one), + measure: loop_infer_atom(s: ^loop_infer_unregistered_measure) + ) + match loop_infer_run(root: body) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn loop_infer_missing_measure_is_refused() -> Bool { + let body = Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: loop_infer_atom(s: ^dag_pick_lit_one) } + ], + occurrence_id: SyntheticOccurrence + } + match loop_infer_run(root: body) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} diff --git a/src/v2/test/claim/loop_multiplicity_measure_test.dag b/src/v2/test/claim/loop_multiplicity_measure_test.dag new file mode 100644 index 00000000000..99074088c23 --- /dev/null +++ b/src/v2/test/claim/loop_multiplicity_measure_test.dag @@ -0,0 +1,218 @@ +module v2.test.claim.loop_multiplicity_measure + +import std.termination { DescentEvidence, Strict, NonIncreasing, DescentUnknown } +import v2.std.cardinality { + LoopBound, + MeasureDescentFact, + Multiplicity, + Bounded, + ProvenTermination, + RequiresTerminationProof, + TerminationProof, + loop_bound_witness_for_node, + loop_multiplicity, + loop_multiplicity_with, + measure_descent_fact_registry, + node_multiplicity, + termination_proof_witness_for_node +} +import v2.std.collection { List } +import v2.std.integer { Int } +import v2.std.logic { Bool } +import v2.std.node { + Atom, + ComputationNode, + Conj, + Edge, + Loop, + Named, + Node, + Positional, + Symbol, + SyntheticOccurrence, + TypeNode +} +import v2.std.witness { Holds, Violates, Witness } + +fn lmm_atom(s: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: s } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn lmm_loop_with_measure(measure: Node) -> Node { + Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: lmm_atom(s: ^lmm_body_lit) }, + Edge { label: Named { name: ^loop_bound_edge }, target: measure } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn lmm_loop_without_measure() -> Node { + Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: lmm_atom(s: ^lmm_body_lit) } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn lmm_conj_measure(a: Node, b: Node) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Named { name: ^lmm_dim_left }, target: a }, + Edge { label: Named { name: ^lmm_dim_right }, target: b } + ], + occurrence_id: SyntheticOccurrence + } +} + +data lmm_registry: List = [ + MeasureDescentFact { + measure: ^lmm_strict_dim, + evidence: Strict, + citation: "test fixture: a strictly descending dimension" + }, + MeasureDescentFact { + measure: ^lmm_non_increasing_dim, + evidence: NonIncreasing, + citation: "test fixture: a non-increasing dimension" + } +] + +fn lmm_is_proven(m: Multiplicity) -> Bool { + match m { + ProvenTermination { proof: _ } => true + RequiresTerminationProof => false + Bounded => false + } +} + +fn lmm_is_refused(m: Multiplicity) -> Bool { + match m { + RequiresTerminationProof => true + ProvenTermination { proof: _ } => false + Bounded => false + } +} + +fn lmm_proven_strict_dimension(m: Multiplicity) -> Symbol { + match m { + ProvenTermination { proof } => proof.strict.measured + RequiresTerminationProof => ^lmm_no_proof + Bounded => ^lmm_no_proof + } +} + +fn lmm_proven_non_increasing_count(m: Multiplicity) -> Int { + match m { + ProvenTermination { proof } => count(proof.non_increasing) + RequiresTerminationProof => 0 - 1 + Bounded => 0 - 1 + } +} + +test fn loop_strict_measure_infers_proven_termination() -> Bool { + let m = loop_multiplicity_with( + registry: lmm_registry, + n: lmm_loop_with_measure(measure: lmm_atom(s: ^lmm_strict_dim)) + ) + lmm_is_proven(m: m) && (lmm_proven_strict_dimension(m: m) == ^lmm_strict_dim) +} + +test fn loop_perturbed_measure_is_refused() -> Bool { + lmm_is_refused( + m: loop_multiplicity_with( + registry: lmm_registry, + n: lmm_loop_with_measure(measure: lmm_atom(s: ^lmm_unregistered_dim)) + ) + ) +} + +test fn loop_lone_non_increasing_measure_is_refused() -> Bool { + lmm_is_refused( + m: loop_multiplicity_with( + registry: lmm_registry, + n: lmm_loop_with_measure(measure: lmm_atom(s: ^lmm_non_increasing_dim)) + ) + ) +} + +test fn loop_lexicographic_measure_proves_with_strict_dimension() -> Bool { + let m = loop_multiplicity_with( + registry: lmm_registry, + n: lmm_loop_with_measure( + measure: lmm_conj_measure( + a: lmm_atom(s: ^lmm_strict_dim), + b: lmm_atom(s: ^lmm_non_increasing_dim) + ) + ) + ) + lmm_is_proven(m: m) && (lmm_proven_non_increasing_count(m: m) == 1) +} + +test fn loop_unknown_dimension_poisons_lexicographic_measure() -> Bool { + lmm_is_refused( + m: loop_multiplicity_with( + registry: lmm_registry, + n: lmm_loop_with_measure( + measure: lmm_conj_measure( + a: lmm_atom(s: ^lmm_strict_dim), + b: lmm_atom(s: ^lmm_unregistered_dim) + ) + ) + ) + ) +} + +test fn loop_missing_measure_is_refused() -> Bool { + lmm_is_refused( + m: loop_multiplicity_with(registry: lmm_registry, n: lmm_loop_without_measure()) + ) +} + +fn lmm_termination_holds(w: Witness) -> Bool { + match w { + Holds { value: _ } => true + Violates { diagnostic: _ } => false + } +} + +fn lmm_loop_bound_termination_holds(w: Witness) -> Bool { + match w { + Holds { value: bound } => lmm_termination_holds(w: bound.termination) + Violates { diagnostic: _ } => false + } +} + +test fn live_registry_proves_loop_measure() -> Bool { + let n = lmm_loop_with_measure(measure: lmm_atom(s: ^dag_loop_measure_sym)) + lmm_is_proven(m: loop_multiplicity(n: n)) + && lmm_is_proven(m: node_multiplicity(n: n)) + && lmm_termination_holds(w: termination_proof_witness_for_node(n: n)) + && lmm_loop_bound_termination_holds(w: loop_bound_witness_for_node(n: n)) +} + +test fn nested_unproven_loop_still_poisons_the_fold() -> Bool { + let inner = lmm_loop_with_measure(measure: lmm_atom(s: ^lmm_unregistered_dim)) + let outer = Node { + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: inner }, + Edge { + label: Named { name: ^loop_bound_edge }, + target: lmm_atom(s: ^dag_loop_measure_sym) + } + ], + occurrence_id: SyntheticOccurrence + } + lmm_is_proven(m: loop_multiplicity(n: outer)) + && !lmm_termination_holds(w: termination_proof_witness_for_node(n: outer)) +} From c1737b784fa021b47cb5ddf698a36bd79956f7d4 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 04:27:45 +0000 Subject: [PATCH 2/9] M1+fold-lowering: the un-forked forward fold->Loop desugaring, first slice MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first real piece of the general body producer that replaces the removed cost-shape fork (and, eventually, the hand-rolled MVP1 loop shapes). A surface fold has no dedicated grammar production — it parses as an ordinary call — so its lowering is a SEMANTIC desugaring keyed on the RESOLVED callee identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. Given a resolved fold call (positional children [callee, collection, init, iteration_body]), fold_call_to_loop lifts the iteration body into the canonical seam Loop bounded by the registered fold-iteration measure, and the kept loop_multiplicity derives PROVEN termination from it — the same real derivation the foundation's loop witnesses use, now reached from a fold-call shape. This pins the seam (M1) and lands the desugaring unit (core of M2), verified by execution: fold_call_lowers_to_terminating_loop (proven termination) + short_fold_call_refuses_no_loop_fabricated (fail-closed red control). It is deliberately resolve-agnostic — it consumes an already-resolved fold-call node — so it is the same desugaring the whole-tree body producer will run on real resolved fold calls once corpus resolution is affordable. Remaining toward catching real quadratics: wire this to real resolved corpus source (M2 full), corpus-scale resolution affordability (M4), re-key the accumulator-copy rule to the seam Loop shape (M3). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 12 +++ src/v2/compiler/fold_lowering.dag | 62 ++++++++++++ .../claim/complexity/fold_lowering_test.dag | 95 +++++++++++++++++++ 3 files changed, 169 insertions(+) create mode 100644 src/v2/compiler/fold_lowering.dag create mode 100644 src/v2/test/claim/complexity/fold_lowering_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index 38adfe0f28f..7adf10ff212 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -150,6 +150,18 @@ data commit_gate_roster: List = [ }, surfaces: [GithubActionsCiJob] }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/test/claim/complexity/fold_lowering_test.dag", + check_fns: [ + "fold_call_lowers_to_terminating_loop", + "short_fold_call_refuses_no_loop_fabricated" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, CommitCheckEnrollment { check: CommitWitnessClaim { entry: "src/v2/test/claim/loop_infer_iteration_test.dag", diff --git a/src/v2/compiler/fold_lowering.dag b/src/v2/compiler/fold_lowering.dag new file mode 100644 index 00000000000..ad623135837 --- /dev/null +++ b/src/v2/compiler/fold_lowering.dag @@ -0,0 +1,62 @@ +module v2.compiler.fold_lowering + +import v2.std.collection { Absent, List, Optional, Present, list_at_optional } +import v2.std.diagnostic { + Diagnostic, + ExternalContractUnknown, + Outcome, + Unavailable, + node_locus, + outcome_accepted, + outcome_rejected +} +import v2.std.node { + Atom, + ComputationNode, + Edge, + Loop, + Named, + Node, + Positional, + TypeNode, + node_synthetic +} +import v2.std.node_query { node_positional_child_targets } + +data fold_lowering_note: String = "The un-forked forward lowering for fold — the first slice of the general body producer that replaces both the removed cost-shape fork and the hand-rolled MVP1 shapes. A surface fold has NO dedicated grammar production; it parses as an ordinary call, so its lowering is a SEMANTIC desugaring keyed on the RESOLVED callee identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. A resolved fold call carries positional children [callee, collection, init, iteration_body]; the desugaring lifts the iteration_body into the canonical seam Loop that the kept 04_infer Loop arm types (body : carrier τ → τ) bounded by the fold-iteration measure ^dag_surface_fold_iteration_measure (registered Strict in v2.std.cardinality.measure_descent_fact_registry, so loop_multiplicity derives its termination). Fail-closed: a fold call whose positional arity does not carry an iteration body refuses with the located ^fold_lowering_shape_invalid, never fabricates a loop. This unit is deliberately resolve-agnostic — it consumes an already-resolved fold-call node — so it is the same desugaring the whole-tree body producer will run once corpus resolution is affordable; the caller supplies the resolved node." + +fn fold_iteration_measure_atom() -> Node { + node_synthetic( + kind: TypeNode { connective: Atom { identity: ^dag_surface_fold_iteration_measure } }, + children: [] + ) +} + +fn fold_call_iteration_body(fold_call: Node) -> Optional { + list_at_optional(xs: node_positional_child_targets(node: fold_call), index: 3) +} + +fn fold_lowering_shape_invalid_diagnostic(n: Node) -> Diagnostic { + Diagnostic { + reason: ^fold_lowering_shape_invalid, + at: node_locus(node: n), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn fold_call_to_loop(fold_call: Node) -> Outcome { + match fold_call_iteration_body(fold_call: fold_call) { + Absent => + outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call)) + Present { value: body } => + outcome_accepted( + value: node_synthetic( + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: body }, + Edge { label: Named { name: ^loop_bound_edge }, target: fold_iteration_measure_atom() } + ] + ) + ) + } +} diff --git a/src/v2/test/claim/complexity/fold_lowering_test.dag b/src/v2/test/claim/complexity/fold_lowering_test.dag new file mode 100644 index 00000000000..92dbdef6cd4 --- /dev/null +++ b/src/v2/test/claim/complexity/fold_lowering_test.dag @@ -0,0 +1,95 @@ +module v2.test.claim.complexity.fold_lowering + +import v2.compiler.fold_lowering { fold_call_to_loop } +import v2.std.cardinality { + Bounded, + Multiplicity, + ProvenTermination, + RequiresTerminationProof, + loop_multiplicity +} +import v2.std.collection { List } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.logic { Bool } +import v2.std.node { + Atom, + ComputationNode, + Edge, + Named, + Node, + Positional, + Symbol, + SyntheticOccurrence, + Transform, + TypeNode +} +import v2.std.text { String } + +data fl_witness_note: String = "Grounds the un-forked fold->Loop desugaring (v2.compiler.fold_lowering) by execution: a resolved fold call (Transform with positional children [callee, collection, init, iteration_body]) lowers to the canonical seam Loop, and the kept loop_multiplicity derives PROVEN termination from the fold-iteration measure — the same real derivation the foundation's loop witnesses use, now reached from a fold-call shape rather than a hand-built loop. Red control: a short-arity fold call carrying no iteration body refuses (Rejected), never fabricating a loop. This is the desugaring unit the whole-tree body producer will run on real resolved fold calls once corpus resolution is affordable; the shape it emits is exactly what the accumulator-copy rule will key on." + +fn fl_atom(s: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: s } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn fl_resolved_fold_call(body: Node) -> Node { + Node { + kind: ComputationNode { behavior: Transform }, + children: [ + Edge { label: Positional, target: fl_atom(s: ^fold) }, + Edge { label: Positional, target: fl_atom(s: ^fl_collection) }, + Edge { label: Positional, target: fl_atom(s: ^fl_init) }, + Edge { label: Positional, target: body } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn fl_short_fold_call() -> Node { + Node { + kind: ComputationNode { behavior: Transform }, + children: [ + Edge { label: Positional, target: fl_atom(s: ^fold) }, + Edge { label: Positional, target: fl_atom(s: ^fl_collection) }, + Edge { label: Positional, target: fl_atom(s: ^fl_init) } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn fl_multiplicity_of(o: Outcome) -> Multiplicity { + match o { + Accepted { value: loop, diagnostics: _ } => loop_multiplicity(n: loop) + Rejected { diagnostics: _ } => RequiresTerminationProof + } +} + +fn fl_is_proven(m: Multiplicity) -> Bool { + match m { + ProvenTermination { proof: _ } => true + RequiresTerminationProof => false + Bounded => false + } +} + +fn fl_is_rejected(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +test fn fold_call_lowers_to_terminating_loop() -> Bool { + fl_is_proven( + m: fl_multiplicity_of( + o: fold_call_to_loop(fold_call: fl_resolved_fold_call(body: fl_atom(s: ^fl_body_lit))) + ) + ) +} + +test fn short_fold_call_refuses_no_loop_fabricated() -> Bool { + fl_is_rejected(o: fold_call_to_loop(fold_call: fl_short_fold_call())) +} From 92ad4b402075f89142ceeb0fd94f386291640835 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 06:05:23 +0000 Subject: [PATCH 3/9] grammar: general expression ident head stamps its lexeme, not the token class MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundational name-resolution fix. dag_grammar_primary_expr_core stamped the general expression ident head with StampClass, so a general call's callee came out as ^dag_token_ident — the NAME dropped at parse. That made every operation (fold, contains, list_append, ...) unidentifiable in real code and left resolution nothing to bind: a self-inconsistency in the grammar, since qualified names (dag_grammar_qualified_name_expr) already StampLexeme. Switch that one terminal to dag_grammar_terminal_lexeme, identical to how qualified names already carry their name. Now a general call carries its callee name, resolution can bind it (resolve_atom looks up the identity in scope), and consumers read the canonical identity the homogeneous way the R1 lens already does (r1_symbol_of = atom.identity, matched against a symbol-keyed registry). This is the existing identification path, not a new mechanism — and NOT the removed fork's post-hoc lexeme-recovery hack (StampLexeme preserves the name AT parse; the hack recovered it from the token stream after the fact). This unblocks operation-identification in real code — the prerequisite for the complexity feature (and general name resolution broadly). v2 is not in production, so this is the right window for the change. Verified: all 4 v2 language parse tests pass; the whole-tree compile-clean gate, emit-host, source-root-ingest, and self-host gates pass (the content-hash ripple is contained); parse floor witness green (parse perf witness runs the v1 parser, unaffected — a transient timing FAIL re-ran green). Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- src/v2/extdeps/languages/dag.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index f788a146713..6c0f6805c92 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -2362,7 +2362,7 @@ fn dag_grammar_primary_expr_expr() -> GrammarExpr { fn dag_grammar_primary_expr_core() -> GrammarExpr { dag_grammar_choice( left: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_ident), + left: dag_grammar_terminal_lexeme(token_class: ^dag_token_ident), right: dag_grammar_primary_ident_suffix_expr() ), right: dag_grammar_choice( From 95b7051df6f2fbf313afecb60ccd9c976fb6bec9 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 06:18:38 +0000 Subject: [PATCH 4/9] M2 verification: fold callee name survives parse on real source MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First check on real source that the StampLexeme grammar fix does its job: a real fold snippet ingested through the census path (tokenize -> parse_module -> normalize, v2.lens.enforcement.cost_coverage) yields a tree in which ^fold (the callee) and ^xs (the collection) appear as atom identities — the names survive, so operation recognition is now possible the homogeneous way the R1 lens reads atom.identity. fold_callee_name_survives_parse is the RED control the pre-fix StampClass regression breaks. CI-enrolled. Grounding note recorded for the next slice: the fold call is NOT shaped as a head-positional callee (that probe failed); it carries the surface call production structure, so the desugaring will navigate it homogeneously via parse_subtree_find_production_captured (the same helper cost_coverage already uses to locate fn bodies) to extract the fn-literal iteration body, then desugar via v2.compiler.fold_lowering. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 13 +++++ .../complexity/fold_real_source_test.dag | 53 +++++++++++++++++++ 2 files changed, 66 insertions(+) create mode 100644 src/v2/test/claim/complexity/fold_real_source_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index 7adf10ff212..f5f12adccad 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -162,6 +162,19 @@ data commit_gate_roster: List = [ }, surfaces: [GithubActionsCiJob] }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/test/claim/complexity/fold_real_source_test.dag", + check_fns: [ + "fold_probe_ingest_is_accepted", + "fold_callee_name_survives_parse", + "fold_collection_name_survives_parse" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, CommitCheckEnrollment { check: CommitWitnessClaim { entry: "src/v2/test/claim/loop_infer_iteration_test.dag", diff --git a/src/v2/test/claim/complexity/fold_real_source_test.dag b/src/v2/test/claim/complexity/fold_real_source_test.dag new file mode 100644 index 00000000000..7e1032a5c04 --- /dev/null +++ b/src/v2/test/claim/complexity/fold_real_source_test.dag @@ -0,0 +1,53 @@ +module v2.test.claim.complexity.fold_real_source + +import std.algebra { Cons, Empty } +import v2.lens.enforcement.cost_coverage { cost_coverage_ingest_source_text } +import v2.std.collection { Absent, List, Optional, Present } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.grammar { node_atom_identity_optional } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.text { String } + +data fold_real_source_note: String = "Grounds the grammar StampLexeme fix on REAL source: after tokenize -> parse_module -> normalize (the census ingest), the callee of a general fold call carries its NAME as an atom identity — ^fold, interned from the lexeme — so operation recognition works the homogeneous way the R1 lens reads atom.identity. Before the fix the callee was ^dag_token_ident (name dropped), so fold_callee_name_survives_parse is the RED control that regression breaks. The collection name (^xs) is checked too, confirming the whole general-ident path carries lexemes, not just the head. Next slice: navigate the surface call production (parse_subtree_find_production_captured, as cost_coverage already locates fn bodies) to extract the fn-literal iteration body and desugar via v2.compiler.fold_lowering." + +data fold_snippet: String = "module fold_probe\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" + +fn collect_atom_identities(n: Node, acc: List) -> List { + let acc1 = match node_atom_identity_optional(node: n) { + Present { value: s } => Cons { head: s, tail: acc } + Absent => acc + } + fold(n.children, init: acc1, f: fn(a, e) { + collect_atom_identities(n: e.target, acc: a) + }) +} + +fn symbol_in(needle: Symbol, xs: List) -> Bool { + fold(xs, init: false, f: fn(acc, s) { + if acc { true } else { s == needle } + }) +} + +fn ingest_identities() -> List { + match cost_coverage_ingest_source_text(source_text: fold_snippet, file: ^fold_probe_file) { + Accepted { value: tree, diagnostics: _ } => + collect_atom_identities(n: tree, acc: Empty) + Rejected { diagnostics: _ } => Empty + } +} + +test fn fold_probe_ingest_is_accepted() -> Bool { + match cost_coverage_ingest_source_text(source_text: fold_snippet, file: ^fold_probe_file) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +test fn fold_callee_name_survives_parse() -> Bool { + symbol_in(needle: ^fold, xs: ingest_identities()) +} + +test fn fold_collection_name_survives_parse() -> Bool { + symbol_in(needle: ^xs, xs: ingest_identities()) +} From 816d9aa188ab303f23bdca5d8e332511e991db57 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 06:53:51 +0000 Subject: [PATCH 5/9] M2: fold->Loop desugaring reads the real surface fold-call shape MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Correct fold_call_to_loop to consume the actual surface fold-call subtree (the primary_expr captured child) rather than a guessed ComputationNode-with-positional-children shape whose index-3 body slot was wrong for real folds (fold's iteration body is a NAMED fn-literal arg, not positional[3]). The desugaring now identifies the call homogeneously: - fold_call_head_symbol reads the sequence-left head projection (the callee ^fold), the same way the qualified-name parser reads sequence heads; - fold_call_iteration_body locates the sole ^dag_surface_fn_literal argument and lifts its ^dag_surface_fn_body, the same way cost_coverage locates fn bodies (parse_subtree_find_production_captured). Keyed on the callee identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. Fail-closed twice: a call whose head is not ^fold refuses (^fold_lowering_not_a_fold_call); a fold call carrying no fn-literal iteration body refuses (^fold_lowering_shape_invalid) — never fabricates a loop. Verified end-to-end on real source through the census ingest (tokenize -> parse_module -> normalize): fold(xs, init: 0, f: fn(acc, x) { acc }) lowers to the canonical seam Loop and loop_multiplicity derives PROVEN termination from the fold-iteration measure. Both fail-closed arms proven discriminating by perturbation (each red control flips to FAIL when its arm is defeated). Consolidate the two probe test files into one end-to-end witness (fold_lowering_test), folding in the StampLexeme survival checks (^fold/^xs survive parse) as the grammar red control; drop the now-redundant fold_real_source_test and update the CI witness roster. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 17 +- src/v2/compiler/fold_lowering.dag | 77 +++++++-- .../claim/complexity/fold_lowering_test.dag | 156 ++++++++++++------ .../complexity/fold_real_source_test.dag | 53 ------ 4 files changed, 168 insertions(+), 135 deletions(-) delete mode 100644 src/v2/test/claim/complexity/fold_real_source_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index f5f12adccad..75b5dc19708 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -153,22 +153,13 @@ data commit_gate_roster: List = [ CommitCheckEnrollment { check: CommitWitnessClaim { entry: "src/v2/test/claim/complexity/fold_lowering_test.dag", - check_fns: [ - "fold_call_lowers_to_terminating_loop", - "short_fold_call_refuses_no_loop_fabricated" - ], - kind: CorpusWitnessKind, - span: SpanUndeclared - }, - surfaces: [GithubActionsCiJob] - }, - CommitCheckEnrollment { - check: CommitWitnessClaim { - entry: "src/v2/test/claim/complexity/fold_real_source_test.dag", check_fns: [ "fold_probe_ingest_is_accepted", "fold_callee_name_survives_parse", - "fold_collection_name_survives_parse" + "fold_collection_name_survives_parse", + "fold_call_lowers_to_terminating_loop", + "non_fold_call_refuses", + "bodyless_fold_call_refuses_no_loop_fabricated" ], kind: CorpusWitnessKind, span: SpanUndeclared diff --git a/src/v2/compiler/fold_lowering.dag b/src/v2/compiler/fold_lowering.dag index ad623135837..454595fad0e 100644 --- a/src/v2/compiler/fold_lowering.dag +++ b/src/v2/compiler/fold_lowering.dag @@ -1,15 +1,23 @@ module v2.compiler.fold_lowering -import v2.std.collection { Absent, List, Optional, Present, list_at_optional } +import v2.extdeps.languages.dag { + ParseSubtreeAbsent, + ParseSubtreeFound, + parse_subtree_find_production_captured +} +import v2.std.collection { Absent, Optional, Present } import v2.std.diagnostic { + Accepted, Diagnostic, ExternalContractUnknown, Outcome, + Rejected, Unavailable, node_locus, outcome_accepted, outcome_rejected } +import v2.std.grammar { node_atom_identity_optional } import v2.std.node { Atom, ComputationNode, @@ -18,12 +26,13 @@ import v2.std.node { Named, Node, Positional, + Symbol, TypeNode, node_synthetic } -import v2.std.node_query { node_positional_child_targets } +import v2.std.node_query { find_named_child } -data fold_lowering_note: String = "The un-forked forward lowering for fold — the first slice of the general body producer that replaces both the removed cost-shape fork and the hand-rolled MVP1 shapes. A surface fold has NO dedicated grammar production; it parses as an ordinary call, so its lowering is a SEMANTIC desugaring keyed on the RESOLVED callee identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. A resolved fold call carries positional children [callee, collection, init, iteration_body]; the desugaring lifts the iteration_body into the canonical seam Loop that the kept 04_infer Loop arm types (body : carrier τ → τ) bounded by the fold-iteration measure ^dag_surface_fold_iteration_measure (registered Strict in v2.std.cardinality.measure_descent_fact_registry, so loop_multiplicity derives its termination). Fail-closed: a fold call whose positional arity does not carry an iteration body refuses with the located ^fold_lowering_shape_invalid, never fabricates a loop. This unit is deliberately resolve-agnostic — it consumes an already-resolved fold-call node — so it is the same desugaring the whole-tree body producer will run once corpus resolution is affordable; the caller supplies the resolved node." +data fold_lowering_note: String = "The un-forked forward lowering for fold — the first slice of the general body producer that replaces both the removed cost-shape fork and the hand-rolled MVP shapes. A surface fold has NO dedicated grammar production; it parses as an ordinary call (a ^dag_surface_primary_expr whose head ident, after the StampLexeme grammar fix, carries its NAME as an atom identity), so its lowering is a SEMANTIC desugaring keyed on the CALLEE identity (DESIGN §4: fold/recursion is sugar over Loop), never a lexeme scan. The input is the fold-call surface subtree — the primary_expr captured child, a sequence(head_ident, call_suffix) — read the homogeneous way cost_coverage locates fn bodies and the qualified-name parser reads sequence heads: fold_call_head_symbol reads the sequence-left head projection (the callee ^fold); fold_call_iteration_body finds the sole ^dag_surface_fn_literal argument and lifts its ^dag_surface_fn_body into the canonical seam Loop (matching body_producer_loop_body) bounded by the fold-iteration measure ^dag_surface_fold_iteration_measure (registered Strict in v2.std.cardinality.measure_descent_fact_registry, so loop_multiplicity derives its termination). Fail-closed twice: a call whose head is not ^fold refuses with ^fold_lowering_not_a_fold_call, and a fold call carrying no fn-literal iteration body refuses with ^fold_lowering_shape_invalid — never fabricates a loop. Verified end-to-end on real source (v2.test.claim.complexity.fold_lowering): fold(xs, init: 0, f: fn(acc, x) { acc }) lowers to a terminating Loop. This unit is the same desugaring the whole-tree body producer will run on every located fold call once corpus resolution/walking is affordable; the caller supplies the located call subtree." fn fold_iteration_measure_atom() -> Node { node_synthetic( @@ -32,8 +41,33 @@ fn fold_iteration_measure_atom() -> Node { ) } +fn fold_call_head_symbol(fold_call: Node) -> Optional { + match find_named_child(root: fold_call, name: ^grammar_sequence_left_node_projection) { + Accepted { value: head, diagnostics: _ } => node_atom_identity_optional(node: head) + Rejected { diagnostics: _ } => Absent + } +} + fn fold_call_iteration_body(fold_call: Node) -> Optional { - list_at_optional(xs: node_positional_child_targets(node: fold_call), index: 3) + match parse_subtree_find_production_captured(root: fold_call, emitted: ^dag_surface_fn_literal) { + ParseSubtreeAbsent => Absent + ParseSubtreeFound { captured: fn_literal } => + match parse_subtree_find_production_captured( + root: fn_literal, + emitted: ^dag_surface_fn_body + ) { + ParseSubtreeAbsent => Absent + ParseSubtreeFound { captured: body } => Present { value: body } + } + } +} + +fn fold_lowering_not_a_fold_call_diagnostic(n: Node) -> Diagnostic { + Diagnostic { + reason: ^fold_lowering_not_a_fold_call, + at: node_locus(node: n), + correction: Unavailable { reason: ExternalContractUnknown } + } } fn fold_lowering_shape_invalid_diagnostic(n: Node) -> Diagnostic { @@ -44,19 +78,30 @@ fn fold_lowering_shape_invalid_diagnostic(n: Node) -> Diagnostic { } } +fn fold_call_seam_loop(body: Node) -> Node { + node_synthetic( + kind: ComputationNode { behavior: Loop }, + children: [ + Edge { label: Positional, target: body }, + Edge { label: Named { name: ^loop_bound_edge }, target: fold_iteration_measure_atom() } + ] + ) +} + fn fold_call_to_loop(fold_call: Node) -> Outcome { - match fold_call_iteration_body(fold_call: fold_call) { + match fold_call_head_symbol(fold_call: fold_call) { Absent => - outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call)) - Present { value: body } => - outcome_accepted( - value: node_synthetic( - kind: ComputationNode { behavior: Loop }, - children: [ - Edge { label: Positional, target: body }, - Edge { label: Named { name: ^loop_bound_edge }, target: fold_iteration_measure_atom() } - ] - ) - ) + outcome_rejected(d: fold_lowering_not_a_fold_call_diagnostic(n: fold_call)) + Present { value: head } => + if head == ^fold { + match fold_call_iteration_body(fold_call: fold_call) { + Absent => + outcome_rejected(d: fold_lowering_shape_invalid_diagnostic(n: fold_call)) + Present { value: body } => + outcome_accepted(value: fold_call_seam_loop(body: body)) + } + } else { + outcome_rejected(d: fold_lowering_not_a_fold_call_diagnostic(n: fold_call)) + } } } diff --git a/src/v2/test/claim/complexity/fold_lowering_test.dag b/src/v2/test/claim/complexity/fold_lowering_test.dag index 92dbdef6cd4..12caf4f5583 100644 --- a/src/v2/test/claim/complexity/fold_lowering_test.dag +++ b/src/v2/test/claim/complexity/fold_lowering_test.dag @@ -1,6 +1,16 @@ module v2.test.claim.complexity.fold_lowering +import std.algebra { Cons, Empty } import v2.compiler.fold_lowering { fold_call_to_loop } +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + ParseSubtreeAbsent, + ParseSubtreeFound, + dag_language_model_wave1, + parse_subtree_find_production_captured +} import v2.std.cardinality { Bounded, Multiplicity, @@ -8,66 +18,52 @@ import v2.std.cardinality { RequiresTerminationProof, loop_multiplicity } -import v2.std.collection { List } +import v2.std.collection { Absent, List, Optional, Present } import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.grammar { node_atom_identity_optional } import v2.std.logic { Bool } -import v2.std.node { - Atom, - ComputationNode, - Edge, - Named, - Node, - Positional, - Symbol, - SyntheticOccurrence, - Transform, - TypeNode -} +import v2.std.node { Node, Symbol } import v2.std.text { String } -data fl_witness_note: String = "Grounds the un-forked fold->Loop desugaring (v2.compiler.fold_lowering) by execution: a resolved fold call (Transform with positional children [callee, collection, init, iteration_body]) lowers to the canonical seam Loop, and the kept loop_multiplicity derives PROVEN termination from the fold-iteration measure — the same real derivation the foundation's loop witnesses use, now reached from a fold-call shape rather than a hand-built loop. Red control: a short-arity fold call carrying no iteration body refuses (Rejected), never fabricating a loop. This is the desugaring unit the whole-tree body producer will run on real resolved fold calls once corpus resolution is affordable; the shape it emits is exactly what the accumulator-copy rule will key on." +data fold_lowering_witness_note: String = "Grounds the un-forked fold->Loop desugaring (v2.compiler.fold_lowering) by execution on REAL source, end-to-end through the census ingest (tokenize -> parse_module -> normalize). A surface fold parses as an ordinary call; after the StampLexeme grammar fix its callee carries its NAME (^fold) as an atom identity and the collection likewise (^xs) — the survival sub-facts are the RED control that a grammar regression (head stamped as the token class) breaks. The located fold-call subtree (the first primary_expr capture — the outermost fn-body expression) desugars to the canonical seam Loop, and the kept loop_multiplicity derives PROVEN termination from the fold-iteration measure — the same real derivation the foundation's loop witnesses use, now reached from a real parsed fold call rather than a hand-built loop. Two fail-closed red controls: a non-fold call (head ^g) refuses (never desugars a foreign call), and a fold call carrying no fn-literal iteration body refuses (never fabricates a loop). This is the desugaring the whole-tree body producer will run on every located fold call once corpus walking is affordable; the shape it emits is exactly what the accumulator-copy rule (M3) will key on." -fn fl_atom(s: Symbol) -> Node { - Node { - kind: TypeNode { connective: Atom { identity: s } }, - children: [], - occurrence_id: SyntheticOccurrence - } -} +data fold_snippet: String = "module fold_probe\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" -fn fl_resolved_fold_call(body: Node) -> Node { - Node { - kind: ComputationNode { behavior: Transform }, - children: [ - Edge { label: Positional, target: fl_atom(s: ^fold) }, - Edge { label: Positional, target: fl_atom(s: ^fl_collection) }, - Edge { label: Positional, target: fl_atom(s: ^fl_init) }, - Edge { label: Positional, target: body } - ], - occurrence_id: SyntheticOccurrence +data non_fold_snippet: String = "module g_probe\n\nfn f(xs: List) -> Int {\n g(xs, f: fn(acc, x) { acc })\n}\n" + +data bodyless_fold_snippet: String = "module bodyless_probe\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0)\n}\n" + +fn ingest(source_text: String, file: Symbol) -> Optional { + let lm = dag_language_model_wave1() + match tokenize(text: source_text, file: file, rules: lm.lex) { + Rejected { diagnostics: _ } => Absent + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => + match normalize(parse_tree: artifact.tree) { + Rejected { diagnostics: _ } => Absent + Accepted { value: tree, diagnostics: _ } => Present { value: tree } + } + } } } -fn fl_short_fold_call() -> Node { - Node { - kind: ComputationNode { behavior: Transform }, - children: [ - Edge { label: Positional, target: fl_atom(s: ^fold) }, - Edge { label: Positional, target: fl_atom(s: ^fl_collection) }, - Edge { label: Positional, target: fl_atom(s: ^fl_init) } - ], - occurrence_id: SyntheticOccurrence +fn locate_call(root: Node) -> Optional { + match parse_subtree_find_production_captured(root: root, emitted: ^dag_surface_primary_expr) { + ParseSubtreeFound { captured: call } => Present { value: call } + ParseSubtreeAbsent => Absent } } -fn fl_multiplicity_of(o: Outcome) -> Multiplicity { - match o { - Accepted { value: loop, diagnostics: _ } => loop_multiplicity(n: loop) - Rejected { diagnostics: _ } => RequiresTerminationProof +fn ingest_and_locate(source_text: String, file: Symbol) -> Optional { + match ingest(source_text: source_text, file: file) { + Absent => Absent + Present { value: tree } => locate_call(root: tree) } } -fn fl_is_proven(m: Multiplicity) -> Bool { +fn is_proven_termination(m: Multiplicity) -> Bool { match m { ProvenTermination { proof: _ } => true RequiresTerminationProof => false @@ -75,21 +71,75 @@ fn fl_is_proven(m: Multiplicity) -> Bool { } } -fn fl_is_rejected(o: Outcome) -> Bool { +fn outcome_is_rejected(o: Outcome) -> Bool { match o { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } } +fn collect_atom_identities(n: Node, acc: List) -> List { + let acc1 = match node_atom_identity_optional(node: n) { + Present { value: s } => Cons { head: s, tail: acc } + Absent => acc + } + fold(n.children, init: acc1, f: fn(a, e) { + collect_atom_identities(n: e.target, acc: a) + }) +} + +fn symbol_in(needle: Symbol, xs: List) -> Bool { + fold(xs, init: false, f: fn(acc, s) { + if acc { true } else { s == needle } + }) +} + +fn fold_snippet_identities() -> List { + match ingest(source_text: fold_snippet, file: ^fold_probe_file) { + Absent => Empty + Present { value: tree } => collect_atom_identities(n: tree, acc: Empty) + } +} + +test fn fold_probe_ingest_is_accepted() -> Bool { + match ingest(source_text: fold_snippet, file: ^fold_probe_file) { + Absent => false + Present { value: _ } => true + } +} + +test fn fold_callee_name_survives_parse() -> Bool { + symbol_in(needle: ^fold, xs: fold_snippet_identities()) +} + +test fn fold_collection_name_survives_parse() -> Bool { + symbol_in(needle: ^xs, xs: fold_snippet_identities()) +} + test fn fold_call_lowers_to_terminating_loop() -> Bool { - fl_is_proven( - m: fl_multiplicity_of( - o: fold_call_to_loop(fold_call: fl_resolved_fold_call(body: fl_atom(s: ^fl_body_lit))) - ) - ) + match ingest_and_locate(source_text: fold_snippet, file: ^fold_probe_file) { + Absent => false + Present { value: call } => + match fold_call_to_loop(fold_call: call) { + Accepted { value: loop, diagnostics: _ } => + is_proven_termination(m: loop_multiplicity(n: loop)) + Rejected { diagnostics: _ } => false + } + } +} + +test fn non_fold_call_refuses() -> Bool { + match ingest_and_locate(source_text: non_fold_snippet, file: ^g_probe_file) { + Absent => false + Present { value: call } => + outcome_is_rejected(o: fold_call_to_loop(fold_call: call)) + } } -test fn short_fold_call_refuses_no_loop_fabricated() -> Bool { - fl_is_rejected(o: fold_call_to_loop(fold_call: fl_short_fold_call())) +test fn bodyless_fold_call_refuses_no_loop_fabricated() -> Bool { + match ingest_and_locate(source_text: bodyless_fold_snippet, file: ^bodyless_probe_file) { + Absent => false + Present { value: call } => + outcome_is_rejected(o: fold_call_to_loop(fold_call: call)) + } } diff --git a/src/v2/test/claim/complexity/fold_real_source_test.dag b/src/v2/test/claim/complexity/fold_real_source_test.dag deleted file mode 100644 index 7e1032a5c04..00000000000 --- a/src/v2/test/claim/complexity/fold_real_source_test.dag +++ /dev/null @@ -1,53 +0,0 @@ -module v2.test.claim.complexity.fold_real_source - -import std.algebra { Cons, Empty } -import v2.lens.enforcement.cost_coverage { cost_coverage_ingest_source_text } -import v2.std.collection { Absent, List, Optional, Present } -import v2.std.diagnostic { Accepted, Outcome, Rejected } -import v2.std.grammar { node_atom_identity_optional } -import v2.std.logic { Bool } -import v2.std.node { Node, Symbol } -import v2.std.text { String } - -data fold_real_source_note: String = "Grounds the grammar StampLexeme fix on REAL source: after tokenize -> parse_module -> normalize (the census ingest), the callee of a general fold call carries its NAME as an atom identity — ^fold, interned from the lexeme — so operation recognition works the homogeneous way the R1 lens reads atom.identity. Before the fix the callee was ^dag_token_ident (name dropped), so fold_callee_name_survives_parse is the RED control that regression breaks. The collection name (^xs) is checked too, confirming the whole general-ident path carries lexemes, not just the head. Next slice: navigate the surface call production (parse_subtree_find_production_captured, as cost_coverage already locates fn bodies) to extract the fn-literal iteration body and desugar via v2.compiler.fold_lowering." - -data fold_snippet: String = "module fold_probe\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" - -fn collect_atom_identities(n: Node, acc: List) -> List { - let acc1 = match node_atom_identity_optional(node: n) { - Present { value: s } => Cons { head: s, tail: acc } - Absent => acc - } - fold(n.children, init: acc1, f: fn(a, e) { - collect_atom_identities(n: e.target, acc: a) - }) -} - -fn symbol_in(needle: Symbol, xs: List) -> Bool { - fold(xs, init: false, f: fn(acc, s) { - if acc { true } else { s == needle } - }) -} - -fn ingest_identities() -> List { - match cost_coverage_ingest_source_text(source_text: fold_snippet, file: ^fold_probe_file) { - Accepted { value: tree, diagnostics: _ } => - collect_atom_identities(n: tree, acc: Empty) - Rejected { diagnostics: _ } => Empty - } -} - -test fn fold_probe_ingest_is_accepted() -> Bool { - match cost_coverage_ingest_source_text(source_text: fold_snippet, file: ^fold_probe_file) { - Accepted { value: _, diagnostics: _ } => true - Rejected { diagnostics: _ } => false - } -} - -test fn fold_callee_name_survives_parse() -> Bool { - symbol_in(needle: ^fold, xs: ingest_identities()) -} - -test fn fold_collection_name_survives_parse() -> Bool { - symbol_in(needle: ^xs, xs: ingest_identities()) -} From 6bbd530f4d1f497d954b40d9db36b3260fe8856b Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 08:45:12 +0000 Subject: [PATCH 6/9] M3: distill a real fold body into R1's fold-step subject; catch a real quadratic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deliver the accumulator-copy lens's first real-source consumer: a surface projection that reads a parsed fold call and builds R1's fold-step subject (Instantiation[acc_binder, combiner, call[port0, port1]]), so R1 catches a real quadratic end-to-end instead of only judging synthetic fixtures. This is the peer projection of M2's fold_call_to_loop (DESIGN §2 Realization: one surface fold call, N consumers — the loop projection is for termination, this one for cost/copy-detection). Both read the SAME located fold call through the SAME fn-literal locator, now factored out as v2.compiler.fold_lowering.fold_call_step_fn (§3 single authority for "where the step function is"). Foundational grammar fix: fn-literal parameters were stamped as the token class (^dag_token_ident), dropping their names — the same StampLexeme drop already fixed for call heads. Verified by execution: an unused param vanished before the fix, survives after. R1 needs the accumulator's name (param 0) to check whether it lands in the combiner's copied port, so the name must survive parse. The distiller (v2.lens.complexity_r1_accumulator_copy.surface_subject) reads four symbols at the surface/lexeme level: acc_binder = step-fn param 0; combiner = the head of the call in the step-fn body; port0/port1 = that call's first two argument values in declared order. Fail-closed at every step: no step fn / no first param / body not a two-argument call / an argument not a bare name all REFUSE with a located diagnostic — never fabricate a subject a fold R1 cannot read as clean. Proven end-to-end on real source (v2.test.claim.complexity.r1_surface_subject), through the census ingest: fold(..., fn(acc, x) { list_append(left: acc, right: x) }) projects Poly(2); the SAME combiner with the accumulator flipped to the non-copied port (list_append(left: x, right: acc)) is clean — isolating the copied-port check as the sole difference; an identity-body fold refuses. Discrimination proven by perturbation: a bogus acc_binder flips the quadratic to clean (acc_binder is read independently, not circularly). Surface-level because corpus resolution/body-production is not yet affordable; a resolved-body read supersedes this once it is, with the seam (fold_call_step_fn) unchanged. Whole-corpus enrollment (sweep every fold, not these snippets) remains future work. Full CI floor green (4 batches, 30 witnesses). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 13 ++ src/v2/compiler/fold_lowering.dag | 11 +- src/v2/extdeps/languages/dag.dag | 2 +- .../lens/complexity_r1_accumulator_copy.dag | 2 +- .../surface_subject.dag | 164 ++++++++++++++++++ .../complexity/r1_surface_subject_test.dag | 108 ++++++++++++ 6 files changed, 296 insertions(+), 4 deletions(-) create mode 100644 src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag create mode 100644 src/v2/test/claim/complexity/r1_surface_subject_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index 75b5dc19708..dc72e27f7ea 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -166,6 +166,19 @@ data commit_gate_roster: List = [ }, surfaces: [GithubActionsCiJob] }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/test/claim/complexity/r1_surface_subject_test.dag", + check_fns: [ + "quadratic_fold_projects_poly_two", + "linear_fold_is_clean", + "identity_body_fold_refuses" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, CommitCheckEnrollment { check: CommitWitnessClaim { entry: "src/v2/test/claim/loop_infer_iteration_test.dag", diff --git a/src/v2/compiler/fold_lowering.dag b/src/v2/compiler/fold_lowering.dag index 454595fad0e..2f460be862b 100644 --- a/src/v2/compiler/fold_lowering.dag +++ b/src/v2/compiler/fold_lowering.dag @@ -48,10 +48,17 @@ fn fold_call_head_symbol(fold_call: Node) -> Optional { } } -fn fold_call_iteration_body(fold_call: Node) -> Optional { +fn fold_call_step_fn(fold_call: Node) -> Optional { match parse_subtree_find_production_captured(root: fold_call, emitted: ^dag_surface_fn_literal) { + ParseSubtreeFound { captured: fn_literal } => Present { value: fn_literal } ParseSubtreeAbsent => Absent - ParseSubtreeFound { captured: fn_literal } => + } +} + +fn fold_call_iteration_body(fold_call: Node) -> Optional { + match fold_call_step_fn(fold_call: fold_call) { + Absent => Absent + Present { value: fn_literal } => match parse_subtree_find_production_captured( root: fn_literal, emitted: ^dag_surface_fn_body diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 6c0f6805c92..849a32b7399 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -2302,7 +2302,7 @@ fn dag_grammar_expr_list_helper() -> GrammarExpr { } fn dag_grammar_untyped_params_helper() -> GrammarExpr { - dag_grammar_comma_list_expr(item: dag_grammar_terminal(token_class: ^dag_token_ident)) + dag_grammar_comma_list_expr(item: dag_grammar_terminal_lexeme(token_class: ^dag_token_ident)) } fn dag_grammar_postfix_call_suffix_expr() -> GrammarExpr { diff --git a/src/v2/lens/complexity_r1_accumulator_copy.dag b/src/v2/lens/complexity_r1_accumulator_copy.dag index d787b450be6..fa8cbc1565d 100644 --- a/src/v2/lens/complexity_r1_accumulator_copy.dag +++ b/src/v2/lens/complexity_r1_accumulator_copy.dag @@ -35,7 +35,7 @@ import v2.std.node { import v2.std.text { String } import v2.std.witness { Holds, Violates, Witness } -data complexity_r1_corpus_census_recall_note: String = "RECALL: future whole-corpus census must rediscover survey suspects — src/v2/workflow/glob_discovery_law.dag:63,94,115 (list_append left:acc); ~10 src/v2/compiler/06_translate.dag list_append(partial,…) sites; v2.std.decl_index.decl_facts_fn_items (fractal: the decl_facts walk itself burned 3m41s in step-0). E2-prep is synthetic Node fixtures only; enrollment waits on E1a body access + enforcement-intent gate." +data complexity_r1_corpus_census_recall_note: String = "RECALL: future whole-corpus census must rediscover survey suspects — src/v2/workflow/glob_discovery_law.dag:63,94,115 (list_append left:acc); ~10 src/v2/compiler/06_translate.dag list_append(partial,…) sites; v2.std.decl_index.decl_facts_fn_items (fractal: the decl_facts walk itself burned 3m41s in step-0). E2-prep is synthetic Node fixtures; E1a body access LANDED surface-level (v2.lens.complexity_r1_accumulator_copy.surface_subject.fold_call_to_r1_subject distills a real parsed fold body into the fold-step subject — proven end-to-end catching a real list_append(left:acc) quadratic in v2.test.claim.complexity.r1_surface_subject); whole-corpus enrollment (sweep every fold, not fixtures) still waits on affected-set/resolution affordability + the enforcement-intent gate, and a resolved-body read supersedes the surface distiller once body-production is affordable." data copied_port_fact_list_append_left_citation: String = "v2.std.algebra.list_append — left port is fold-over-left copy port (fold_list_right snoc over left)" diff --git a/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag b/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag new file mode 100644 index 00000000000..023aa3543c3 --- /dev/null +++ b/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag @@ -0,0 +1,164 @@ +module v2.lens.complexity_r1_accumulator_copy.surface_subject + +import v2.compiler.fold_lowering { fold_call_step_fn } +import v2.lens.complexity_r1_accumulator_copy { r1_fold_step_subject } +import v2.extdeps.languages.dag { + ParseSubtreeAbsent, + ParseSubtreeFound, + parse_production_captured_child_optional, + parse_production_emitted_identity_optional, + parse_subtree_find_production_captured +} +import std.algebra { Empty } +import v2.std.algebra { list_snoc_item } +import v2.std.collection { Absent, List, Optional, Present, list_at_optional } +import v2.std.diagnostic { + Accepted, + Diagnostic, + ExternalContractUnknown, + Outcome, + Rejected, + Unavailable, + node_locus, + outcome_accepted, + outcome_rejected +} +import v2.std.grammar { node_atom_identity_optional } +import v2.std.integer { Int } +import v2.std.node { Node, Symbol } +import v2.std.node_query { find_named_child } + +data surface_subject_note: String = "Distills a real surface fold call into the R1 accumulator-copy lens's fold-step subject (Instantiation[acc_binder, combiner, call[port0, port1]]) — the peer projection of v2.compiler.fold_lowering.fold_call_to_loop (§2 Realization: one surface fold call, N consumers — the loop projection is for termination, this one is for cost/copy-detection). It reads the SAME located fold call through the SAME fn-literal locator (fold_call_step_fn), then reads four symbols at the surface/lexeme level (post the StampLexeme grammar fixes, so both param decls and call heads carry their names): acc_binder = the step function's FIRST param (the fold accumulator); combiner = the head of the call in the step-fn body; port0/port1 = that call's first two argument values, in declared order. R1 then judges whether acc_binder lands in the combiner's copied port (copied_port_fact_registry). Fail-closed: any missing piece (no step fn, no first param, body is not a two-argument call, an argument value is not a bare name) REFUSES with a located diagnostic — never fabricates a subject, so a fold R1 cannot read never silently reads as clean. This is surface-level (pre-resolve) because corpus resolution/body-production is not yet affordable; when it is, the resolved-body read supersedes this and the seam (fold_call_step_fn) is unchanged. Verified end-to-end on real source (v2.test.claim.complexity.r1_surface_subject): list_append(left: acc, …) projects Poly(2); list_append(right: acc) with acc out of the copied port is clean — same combiner, accumulator position flipped, isolating the copied-port check." + +fn named_child_optional(cap: Node, name: Symbol) -> Optional { + match find_named_child(root: cap, name: name) { + Accepted { value: c, diagnostics: _ } => Present { value: c } + Rejected { diagnostics: _ } => Absent + } +} + +fn sequence_left_node(cap: Node) -> Optional { + named_child_optional(cap: cap, name: ^grammar_sequence_left_node_projection) +} + +fn sequence_right_node(cap: Node) -> Optional { + named_child_optional(cap: cap, name: ^grammar_sequence_right_node_projection) +} + +fn sequence_left_symbol(cap: Node) -> Optional { + match sequence_left_node(cap: cap) { + Absent => Absent + Present { value: left } => node_atom_identity_optional(node: left) + } +} + +fn find_capture(root: Node, emitted: Symbol) -> Optional { + match parse_subtree_find_production_captured(root: root, emitted: emitted) { + ParseSubtreeFound { captured: c } => Present { value: c } + ParseSubtreeAbsent => Absent + } +} + +fn collect_captures(n: Node, emitted: Symbol, acc: List) -> List { + let acc1 = match parse_production_emitted_identity_optional(node: n) { + Present { value: id } => + if id == emitted { + match parse_production_captured_child_optional(node: n) { + Present { value: c } => list_snoc_item(xs: acc, item: c) + Absent => acc + } + } else { + acc + } + Absent => acc + } + fold(n.children, init: acc1, f: fn(a, e) { + collect_captures(n: e.target, emitted: emitted, acc: a) + }) +} + +fn step_fn_first_param_symbol(fn_literal: Node) -> Optional { + match sequence_right_node(cap: fn_literal) { + Absent => Absent + Present { value: after_kw_fn } => + match sequence_right_node(cap: after_kw_fn) { + Absent => Absent + Present { value: after_lparen } => + match sequence_left_node(cap: after_lparen) { + Absent => Absent + Present { value: params } => sequence_left_symbol(cap: params) + } + } + } +} + +fn step_fn_body_call(fn_literal: Node) -> Optional { + match find_capture(root: fn_literal, emitted: ^dag_surface_fn_body) { + Absent => Absent + Present { value: body } => find_capture(root: body, emitted: ^dag_surface_primary_expr) + } +} + +fn body_call_combiner_symbol(body_call: Node) -> Optional { + sequence_left_symbol(cap: body_call) +} + +fn arg_value_symbol(arg_capture: Node) -> Optional { + match find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) { + Absent => Absent + Present { value: value_expr } => sequence_left_symbol(cap: value_expr) + } +} + +fn body_call_port_symbol(body_call: Node, index: Int) -> Optional { + match list_at_optional( + xs: collect_captures(n: body_call, emitted: ^dag_surface_arg, acc: Empty), + index: index + ) { + Absent => Absent + Present { value: arg } => arg_value_symbol(arg_capture: arg) + } +} + +fn surface_subject_shape_invalid_diagnostic(n: Node) -> Diagnostic { + Diagnostic { + reason: ^r1_surface_subject_shape_invalid, + at: node_locus(node: n), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn fold_call_to_r1_subject(fold_call: Node) -> Outcome { + match fold_call_step_fn(fold_call: fold_call) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fold_call)) + Present { value: fn_literal } => + match step_fn_first_param_symbol(fn_literal: fn_literal) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fn_literal)) + Present { value: acc_binder } => + match step_fn_body_call(fn_literal: fn_literal) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fn_literal)) + Present { value: body_call } => + match body_call_combiner_symbol(body_call: body_call) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Present { value: combiner } => + match body_call_port_symbol(body_call: body_call, index: 0) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Present { value: port0 } => + match body_call_port_symbol(body_call: body_call, index: 1) { + Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Present { value: port1 } => + outcome_accepted( + value: r1_fold_step_subject( + acc_binder: acc_binder, + combiner: combiner, + port0_arg: port0, + port1_arg: port1 + ) + ) + } + } + } + } + } + } +} diff --git a/src/v2/test/claim/complexity/r1_surface_subject_test.dag b/src/v2/test/claim/complexity/r1_surface_subject_test.dag new file mode 100644 index 00000000000..a5bca0f42e0 --- /dev/null +++ b/src/v2/test/claim/complexity/r1_surface_subject_test.dag @@ -0,0 +1,108 @@ +module v2.test.claim.complexity.r1_surface_subject + +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.tokenize { tokenize } +import v2.lens.complexity_r1_accumulator_copy { + R1Clean, + R1MalformedSubject, + R1PolyTwoSuspect, + r1_judge_fold_step +} +import v2.lens.complexity_r1_accumulator_copy.surface_subject { fold_call_to_r1_subject } +import v2.extdeps.languages.dag { + ParseSubtreeAbsent, + ParseSubtreeFound, + dag_language_model_wave1, + parse_subtree_find_production_captured +} +import v2.std.collection { Absent, Optional, Present } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.text { String } + +data r1_surface_subject_note: String = "Catches a real quadratic end-to-end: real source -> census ingest (tokenize/parse/normalize) -> locate the fold call -> fold_call_to_r1_subject distills the surface fold body into R1's fold-step subject -> r1_judge_fold_step. The RED (list_append(left: acc, right: x)) has the accumulator in list_append's copied (left) port, so R1 projects Poly(2). The GREEN uses the SAME combiner with the accumulator flipped to the non-copied (right) port (list_append(left: x, right: acc)) — clean — isolating the copied-port check as the sole difference. The REFUSE control is an identity-body fold (fn(acc, x) { acc }) with no two-argument combiner call: the distiller refuses (fail-closed), never fabricating a subject that R1 would read as clean." + +data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" + +data linear_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" + +data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" + +fn ingest(source_text: String, file: Symbol) -> Optional { + let lm = dag_language_model_wave1() + match tokenize(text: source_text, file: file, rules: lm.lex) { + Rejected { diagnostics: _ } => Absent + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => + match normalize(parse_tree: artifact.tree) { + Rejected { diagnostics: _ } => Absent + Accepted { value: tree, diagnostics: _ } => Present { value: tree } + } + } + } +} + +fn locate_fold_call(root: Node) -> Optional { + match parse_subtree_find_production_captured(root: root, emitted: ^dag_surface_primary_expr) { + ParseSubtreeFound { captured: call } => Present { value: call } + ParseSubtreeAbsent => Absent + } +} + +fn located_subject(source_text: String, file: Symbol) -> Optional> { + match ingest(source_text: source_text, file: file) { + Absent => Absent + Present { value: tree } => + match locate_fold_call(root: tree) { + Absent => Absent + Present { value: call } => Present { value: fold_call_to_r1_subject(fold_call: call) } + } + } +} + +test fn quadratic_fold_projects_poly_two() -> Bool { + match located_subject(source_text: quadratic_snippet, file: ^quad_file) { + Absent => false + Present { value: outcome } => + match outcome { + Rejected { diagnostics: _ } => false + Accepted { value: subject, diagnostics: _ } => + match r1_judge_fold_step(n: subject) { + R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true + R1Clean { flow_opaque_count: _ } => false + R1MalformedSubject => false + } + } + } +} + +test fn linear_fold_is_clean() -> Bool { + match located_subject(source_text: linear_snippet, file: ^lin_file) { + Absent => false + Present { value: outcome } => + match outcome { + Rejected { diagnostics: _ } => false + Accepted { value: subject, diagnostics: _ } => + match r1_judge_fold_step(n: subject) { + R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => false + R1Clean { flow_opaque_count: _ } => true + R1MalformedSubject => false + } + } + } +} + +test fn identity_body_fold_refuses() -> Bool { + match located_subject(source_text: identity_snippet, file: ^ident_file) { + Absent => false + Present { value: outcome } => + match outcome { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } + } +} From 4fd82595e8c47f0def3a6b85fb191b2b9789be2a Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 14:04:03 +0000 Subject: [PATCH 7/9] Challenge R1 against real corpus shapes: coverage boundary + per-cause refusals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Following the methodology "run the model on the real system and let where it comes back lacking be the signal it's not done" — challenged the M3 distiller against the actual corpus suspect shape (src/v2/workflow/glob_discovery_law.dag), not the textbook snippet the M3 tests were written around. Finding (verified by execution): the distiller MISSES the real quadratic. The real suspect is fold_list with the copying list_append(left: acc, right: Cons{..}) buried inside an if-branch and a struct-literal grow-by-one arg. The distiller reads only "the first call in the step body" — which is the if-CONDITION, a one-argument call — so it reads the branch condition as the combiner and refuses (cause: port1_opaque) rather than looking inside the branch. Corpus scale for context: ~676 fold + ~413 fold_list + ~37 fold_node calls; the textbook direct- combiner-body shape the distiller handles is the minority. Captured as a committed coverage-boundary witness (real_branch_body_quadratic_is_currently_missed): a RED that flips to FAIL the moment the distiller learns to traverse branches — the flip is the dissolution trigger to widen it into a positive catch. This is the honest "green on the textbook shape, not done on real code" marker. Made the distiller's refusals per-cause (FoldSurfaceRead classification → no_step_fn / no_accumulator_param / body_not_located / body_head_opaque / port0_opaque / port1_opaque), so the gap is a typed, located, legible fact rather than one opaque shape-invalid (DESIGN §5: a refusal must be a typed, located diagnostic). fold_call_to_r1_subject's public Outcome contract is unchanged; the M3 tests pass unchanged. Note: a whole-corpus quantified sweep of the distiller hits the same affordability wall as M4 (per-file ingest + O(folds×subtree) walks), so quantifying at scale waits on that infra; the qualitative finding here is decisive on its own. Full CI floor green (4 batches, 31 witnesses). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 3 +- .../surface_subject.dag | 79 +++++++++++++++---- .../complexity/r1_surface_subject_test.dag | 20 ++++- 3 files changed, 83 insertions(+), 19 deletions(-) diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index dc72e27f7ea..e0c90d0f1db 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -172,7 +172,8 @@ data commit_gate_roster: List = [ check_fns: [ "quadratic_fold_projects_poly_two", "linear_fold_is_clean", - "identity_body_fold_refuses" + "identity_body_fold_refuses", + "real_branch_body_quadratic_is_currently_missed" ], kind: CorpusWitnessKind, span: SpanUndeclared diff --git a/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag b/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag index 023aa3543c3..6de55105630 100644 --- a/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag +++ b/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag @@ -120,41 +120,42 @@ fn body_call_port_symbol(body_call: Node, index: Int) -> Optional { } } -fn surface_subject_shape_invalid_diagnostic(n: Node) -> Diagnostic { - Diagnostic { - reason: ^r1_surface_subject_shape_invalid, - at: node_locus(node: n), - correction: Unavailable { reason: ExternalContractUnknown } - } -} +type FoldSurfaceRead + = FoldSurfaceSubject { subject: Node } + | FoldSurfaceNoStepFn + | FoldSurfaceNoAccumulatorParam + | FoldSurfaceBodyNotLocated + | FoldSurfaceBodyHeadOpaque + | FoldSurfacePort0Opaque + | FoldSurfacePort1Opaque -fn fold_call_to_r1_subject(fold_call: Node) -> Outcome { +fn read_fold_surface(fold_call: Node) -> FoldSurfaceRead { match fold_call_step_fn(fold_call: fold_call) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fold_call)) + Absent => FoldSurfaceNoStepFn Present { value: fn_literal } => match step_fn_first_param_symbol(fn_literal: fn_literal) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fn_literal)) + Absent => FoldSurfaceNoAccumulatorParam Present { value: acc_binder } => match step_fn_body_call(fn_literal: fn_literal) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: fn_literal)) + Absent => FoldSurfaceBodyNotLocated Present { value: body_call } => match body_call_combiner_symbol(body_call: body_call) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Absent => FoldSurfaceBodyHeadOpaque Present { value: combiner } => match body_call_port_symbol(body_call: body_call, index: 0) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Absent => FoldSurfacePort0Opaque Present { value: port0 } => match body_call_port_symbol(body_call: body_call, index: 1) { - Absent => outcome_rejected(d: surface_subject_shape_invalid_diagnostic(n: body_call)) + Absent => FoldSurfacePort1Opaque Present { value: port1 } => - outcome_accepted( - value: r1_fold_step_subject( + FoldSurfaceSubject { + subject: r1_fold_step_subject( acc_binder: acc_binder, combiner: combiner, port0_arg: port0, port1_arg: port1 ) - ) + } } } } @@ -162,3 +163,47 @@ fn fold_call_to_r1_subject(fold_call: Node) -> Outcome { } } } + +fn fold_surface_refusal_reason(read: FoldSurfaceRead) -> Symbol { + match read { + FoldSurfaceSubject { subject: _ } => ^r1_surface_subject_present + FoldSurfaceNoStepFn => ^r1_surface_no_step_fn + FoldSurfaceNoAccumulatorParam => ^r1_surface_no_accumulator_param + FoldSurfaceBodyNotLocated => ^r1_surface_body_not_located + FoldSurfaceBodyHeadOpaque => ^r1_surface_body_head_opaque + FoldSurfacePort0Opaque => ^r1_surface_port0_opaque + FoldSurfacePort1Opaque => ^r1_surface_port1_opaque + } +} + +fn surface_subject_diagnostic(reason: Symbol, n: Node) -> Diagnostic { + Diagnostic { + reason: reason, + at: node_locus(node: n), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn fold_call_to_r1_subject(fold_call: Node) -> Outcome { + match read_fold_surface(fold_call: fold_call) { + FoldSurfaceSubject { subject: subject } => outcome_accepted(value: subject) + FoldSurfaceNoStepFn => + outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_no_step_fn, n: fold_call)) + FoldSurfaceNoAccumulatorParam => + outcome_rejected( + d: surface_subject_diagnostic(reason: ^r1_surface_no_accumulator_param, n: fold_call) + ) + FoldSurfaceBodyNotLocated => + outcome_rejected( + d: surface_subject_diagnostic(reason: ^r1_surface_body_not_located, n: fold_call) + ) + FoldSurfaceBodyHeadOpaque => + outcome_rejected( + d: surface_subject_diagnostic(reason: ^r1_surface_body_head_opaque, n: fold_call) + ) + FoldSurfacePort0Opaque => + outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_port0_opaque, n: fold_call)) + FoldSurfacePort1Opaque => + outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_port1_opaque, n: fold_call)) + } +} diff --git a/src/v2/test/claim/complexity/r1_surface_subject_test.dag b/src/v2/test/claim/complexity/r1_surface_subject_test.dag index a5bca0f42e0..d12558c4d46 100644 --- a/src/v2/test/claim/complexity/r1_surface_subject_test.dag +++ b/src/v2/test/claim/complexity/r1_surface_subject_test.dag @@ -22,7 +22,7 @@ import v2.std.logic { Bool } import v2.std.node { Node, Symbol } import v2.std.text { String } -data r1_surface_subject_note: String = "Catches a real quadratic end-to-end: real source -> census ingest (tokenize/parse/normalize) -> locate the fold call -> fold_call_to_r1_subject distills the surface fold body into R1's fold-step subject -> r1_judge_fold_step. The RED (list_append(left: acc, right: x)) has the accumulator in list_append's copied (left) port, so R1 projects Poly(2). The GREEN uses the SAME combiner with the accumulator flipped to the non-copied (right) port (list_append(left: x, right: acc)) — clean — isolating the copied-port check as the sole difference. The REFUSE control is an identity-body fold (fn(acc, x) { acc }) with no two-argument combiner call: the distiller refuses (fail-closed), never fabricating a subject that R1 would read as clean." +data r1_surface_subject_note: String = "Catches a real quadratic end-to-end: real source -> census ingest (tokenize/parse/normalize) -> locate the fold call -> fold_call_to_r1_subject distills the surface fold body into R1's fold-step subject -> r1_judge_fold_step. The RED (list_append(left: acc, right: x)) has the accumulator in list_append's copied (left) port, so R1 projects Poly(2). The GREEN uses the SAME combiner with the accumulator flipped to the non-copied (right) port (list_append(left: x, right: acc)) — clean — isolating the copied-port check as the sole difference. The REFUSE control is an identity-body fold (fn(acc, x) { acc }) with no two-argument combiner call: the distiller refuses (fail-closed), never fabricating a subject that R1 would read as clean. COVERAGE BOUNDARY (real_branch_body_quadratic_is_currently_missed): challenged against the ACTUAL corpus suspect shape (src/v2/workflow/glob_discovery_law.dag: fold_list with the copying list_append(left: acc, right: Cons{..}) buried inside an if-branch and a struct-literal grow-by-one arg), the distiller MISSES it — verified by execution it refuses with cause port1_opaque because it reads the if-CONDITION (a one-argument call) as the combiner rather than looking inside the branch. That test is a RED that flips to FAIL the moment the distiller learns to traverse branches; the flip is the dissolution trigger to widen this marker into a positive catch. This is the honest signal that the mechanism, though green on the textbook shape, is not yet done on real code." data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" @@ -30,6 +30,8 @@ data linear_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fol data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" +data real_branch_body_snippet: String = "module rs\n\nfn g(xs: List) -> Int {\n fold_list(xs: xs, empty: Empty, cons: fn(acc, r) {\n if pred(r: r) {\n list_append(left: acc, right: Cons { head: r, tail: Empty })\n } else {\n acc\n }\n })\n}\n" + fn ingest(source_text: String, file: Symbol) -> Optional { let lm = dag_language_model_wave1() match tokenize(text: source_text, file: file, rules: lm.lex) { @@ -106,3 +108,19 @@ test fn identity_body_fold_refuses() -> Bool { } } } + +test fn real_branch_body_quadratic_is_currently_missed() -> Bool { + match located_subject(source_text: real_branch_body_snippet, file: ^rs_file) { + Absent => false + Present { value: outcome } => + match outcome { + Rejected { diagnostics: _ } => true + Accepted { value: subject, diagnostics: _ } => + match r1_judge_fold_step(n: subject) { + R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => false + R1Clean { flow_opaque_count: _ } => true + R1MalformedSubject => true + } + } + } +} From 8e396f7b81e659453713b478a29d4c954071f39b Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 9 Jul 2026 17:50:42 +0000 Subject: [PATCH 8/9] Kill the R1 bridge: linear fold over Node, no intermediate subject MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the 230-line surface-navigation distiller (surface_subject.dag) and the bespoke r1_fold_step_subject intermediate with a single linear fold, so the lens is stage1→stage2→… with each stage consuming the previous stage's natural type (a Node), no adapter. Two halves, cleanly split: - COST MODEL (complexity_r1_accumulator_copy.dag) — navigation-free. Owns the copied-port registry lookup and classify_call(at, combiner, port_syms, carriers) → Optional. Finding = Poly2Suspect | AnalysisOpaque. - TRAVERSAL (complexity_r1_accumulator_copy/analyze.dag) — the fold. analyze(node, carriers) recurses over the whole tree threading the carrier environment down: at a fold-family call it binds the step-fn's accumulator; at every combiner call it asks classify_call. Because the fold VISITS every node instead of doing targeted "first call in the body" lookup, a copy inside an if/match/let is found by construction. The real glob_discovery_law shape (fold_list, copying list_append(left: acc, ...) inside an if-branch, grow-by-one struct arg) that the bridge MISSED is now CAUGHT — the old coverage-boundary witness flipped from "currently missed" to real_branch_body_quadratic_is_caught. classify_call reads only the copied port, so the old over-strict "both ports must be bare names" gap is gone too. Ports are read as DIRECT args (no descent into an arg's value) so a nested call doesn't shift the copied-port index (map_merge's copied port is index 1). Fail-closed preserved: a known combiner whose copied port is not a bare name is a counted, located AnalysisOpaque finding — "could not tell" stays distinct from "clean" (DESIGN §5). Deletes surface_subject.dag, the r1_fold_step_subject/r1_judge_fold_step judge, and the 5 synthetic red/green fixtures; the registry coverage they gave is consolidated into a direct classify_call unit test (complexity_r1_accumulator_copy_test) covering list_append/list_snoc/map_merge suspects, non-copied-port and unregistered-combiner cleans, and the opaque case. r1_surface_subject_test → r1_fold_analysis_test (drives the fold end-to-end). Remaining (the follow-on "guessing" discussion): three surface reads inside the fold are still syntactic — carrier = positional first param, combiner = lexeme name, carrier-in-copied-port = symbol equality not dataflow — which want to be edge lookups in a resolved/bound tree. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_018ZJjv8DKX4PpywPNTy6wpc --- dag/gunbc/commit_workflow.dag | 27 ++- .../lens/complexity_r1_accumulator_copy.dag | 219 +++--------------- .../analyze.dag | 203 ++++++++++++++++ .../green_cons_prepend.dag | 55 ----- .../green_merge_envs_base_acc.dag | 55 ----- .../red_compositional_env_union.dag | 55 ----- .../red_list_append_left.dag | 55 ----- .../red_map_merge_overlay_acc.dag | 55 ----- .../surface_subject.dag | 209 ----------------- .../complexity_r1_accumulator_copy_test.dag | 148 +++++++++--- .../complexity/r1_fold_analysis_test.dag | 84 +++++++ .../complexity/r1_surface_subject_test.dag | 126 ---------- 12 files changed, 454 insertions(+), 837 deletions(-) create mode 100644 src/v2/lens/complexity_r1_accumulator_copy/analyze.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/green_cons_prepend.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/green_merge_envs_base_acc.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/red_compositional_env_union.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/red_list_append_left.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/red_map_merge_overlay_acc.dag delete mode 100644 src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag create mode 100644 src/v2/test/claim/complexity/r1_fold_analysis_test.dag delete mode 100644 src/v2/test/claim/complexity/r1_surface_subject_test.dag diff --git a/dag/gunbc/commit_workflow.dag b/dag/gunbc/commit_workflow.dag index e0c90d0f1db..7f54567f6a9 100644 --- a/dag/gunbc/commit_workflow.dag +++ b/dag/gunbc/commit_workflow.dag @@ -168,12 +168,29 @@ data commit_gate_roster: List = [ }, CommitCheckEnrollment { check: CommitWitnessClaim { - entry: "src/v2/test/claim/complexity/r1_surface_subject_test.dag", + entry: "src/v2/test/claim/complexity/r1_fold_analysis_test.dag", check_fns: [ - "quadratic_fold_projects_poly_two", - "linear_fold_is_clean", - "identity_body_fold_refuses", - "real_branch_body_quadratic_is_currently_missed" + "quadratic_fold_has_suspect", + "linear_fold_has_no_suspect", + "identity_fold_has_no_finding", + "real_branch_body_quadratic_is_caught" + ], + kind: CorpusWitnessKind, + span: SpanUndeclared + }, + surfaces: [GithubActionsCiJob] + }, + CommitCheckEnrollment { + check: CommitWitnessClaim { + entry: "src/v2/lens/complexity_r1_accumulator_copy_test.dag", + check_fns: [ + "red_list_append_left_is_suspect", + "red_list_snoc_left_is_suspect", + "red_map_merge_overlay_is_suspect", + "green_map_merge_base_is_clean", + "green_list_append_acc_in_noncopied_port_is_clean", + "green_unregistered_combiner_is_clean", + "opaque_copied_port_is_analysis_opaque" ], kind: CorpusWitnessKind, span: SpanUndeclared diff --git a/src/v2/lens/complexity_r1_accumulator_copy.dag b/src/v2/lens/complexity_r1_accumulator_copy.dag index fa8cbc1565d..7421ff12530 100644 --- a/src/v2/lens/complexity_r1_accumulator_copy.dag +++ b/src/v2/lens/complexity_r1_accumulator_copy.dag @@ -6,36 +6,16 @@ import v2.lens.cost { PolynomialCost, SizeVariable, SymbolicCost, - polynomial_degree_two, - zero_cost + polynomial_degree_two } -import std.algebra { Cons, Empty } -import v2.std.algebra { CopiedPortFact, copied_port_fact_registry, fold_list, list_append } -import v2.std.collection { - List, - Optional, - Present, - Absent, - list_at_optional -} -import v2.std.diagnostic { Diagnostic, Textual, WholeFile, Unavailable, ExternalContractUnknown } +import v2.std.algebra { CopiedPortFact, copied_port_fact_registry, fold_list } +import v2.std.collection { Absent, List, Optional, Present, list_at_optional } import v2.std.integer { Int } import v2.std.logic { Bool } -import v2.std.node { - Atom, - Edge, - Instantiation, - Named, - Node, - Positional, - Symbol, - TypeNode, - SyntheticOccurrence -} +import v2.std.node { Node, Symbol } import v2.std.text { String } -import v2.std.witness { Holds, Violates, Witness } -data complexity_r1_corpus_census_recall_note: String = "RECALL: future whole-corpus census must rediscover survey suspects — src/v2/workflow/glob_discovery_law.dag:63,94,115 (list_append left:acc); ~10 src/v2/compiler/06_translate.dag list_append(partial,…) sites; v2.std.decl_index.decl_facts_fn_items (fractal: the decl_facts walk itself burned 3m41s in step-0). E2-prep is synthetic Node fixtures; E1a body access LANDED surface-level (v2.lens.complexity_r1_accumulator_copy.surface_subject.fold_call_to_r1_subject distills a real parsed fold body into the fold-step subject — proven end-to-end catching a real list_append(left:acc) quadratic in v2.test.claim.complexity.r1_surface_subject); whole-corpus enrollment (sweep every fold, not fixtures) still waits on affected-set/resolution affordability + the enforcement-intent gate, and a resolved-body read supersedes the surface distiller once body-production is affordable." +data complexity_r1_corpus_census_recall_note: String = "RECALL: future whole-corpus census must rediscover survey suspects — src/v2/workflow/glob_discovery_law.dag:63,94,115 (list_append left:acc); ~10 src/v2/compiler/06_translate.dag list_append(partial,…) sites; v2.std.decl_index.decl_facts_fn_items (fractal: the decl_facts walk itself burned 3m41s in step-0). This is the COST MODEL half of the lens — navigation-free: it owns the copied-port registry lookup (r1_copied_port_index) and the per-call classification (classify_call). The traversal half is the linear fold in v2.lens.complexity_r1_accumulator_copy.analyze, which visits every Node, threads the carrier environment, and calls classify_call at each combiner site — so a copy inside an if/match/let is found by construction (the fold visits it), never by targeted lookup. Whole-corpus enrollment (run the fold over every file, not fixtures) still waits on affected-set/resolution affordability + the enforcement-intent gate; a resolved-body read (binding + dataflow edges) supersedes the surface reads the fold does today." data copied_port_fact_list_append_left_citation: String = "v2.std.algebra.list_append — left port is fold-over-left copy port (fold_list_right snoc over left)" @@ -43,42 +23,22 @@ data copied_port_fact_list_snoc_left_citation: String = "v2.std.algebra.list_sno data copied_port_fact_map_merge_overlay_citation: String = "v1_rt.rs:360 rc_map_merge iterates overlay into Rc::make_mut(base); acc in base port is blessed — acc in overlay is R1 copied-port (historical blessed instance: merge_envs, deleted from src/v1/04_env.dag 2026-07-06; a live overlay-port suspect for future census: collect_unit_variant_phantom_matches fold, src/v1/04_resolve.dag)" -data complexity_r1_flow_opaque_residue_note: String = "FlowOpaque: accumulator binder not a direct-reference at either combiner call port (opaque through lets/nested calls). Counted in R1JudgeResult.flow_opaque_count — never silently skipped; lens boundary Violates." +data complexity_r1_opaque_residue_note: String = "AnalysisOpaque: the combiner is a known copied-port row but the copied port's argument is not a bare carrier name (opaque through lets/nested calls/computed expressions). Emitted as a located, counted Finding — never silently dropped, so 'I could not tell' stays distinct from 'clean' (DESIGN §5: ⊤-as-ignorance is not ⊤-as-answer)." -type R1JudgeResult - = R1PolyTwoSuspect { implied_cost: SymbolicCost, flow_opaque_count: Int } - | R1Clean { flow_opaque_count: Int } - | R1MalformedSubject +type Finding + = Poly2Suspect { at: Node, cost: SymbolicCost } + | AnalysisOpaque { at: Node, reason: Symbol } -fn r1_symbol_atom(s: Symbol) -> Node { - Node { - kind: TypeNode { connective: Atom { identity: s } }, - children: [], - occurrence_id: SyntheticOccurrence - } +fn r1_symbols_equal(a: Symbol, b: Symbol) -> Bool { + a == b } -fn r1_positional_targets(n: Node) -> List { - fold(n.children, init: Empty, f: fn(acc, e) { - match e.label { - Positional => - list_append(left: acc, right: Cons { head: e.target, tail: Empty }) - Named { name: _ } => acc - } +fn symbol_in(needle: Symbol, xs: List) -> Bool { + fold(xs, init: false, f: fn(acc, s) { + if acc { true } else { r1_symbols_equal(a: s, b: needle) } }) } -fn r1_symbol_of(n: Node) -> Optional { - match n.kind { - TypeNode { connective: Atom { identity: s } } => Present { value: s } - _ => Absent - } -} - -fn r1_symbols_equal(a: Symbol, b: Symbol) -> Bool { - a == b -} - fn r1_row_matches_combiner(row: CopiedPortFact, combiner: Symbol) -> Bool { r1_symbols_equal(a: row.combiner, b: combiner) } @@ -112,145 +72,36 @@ fn r1_poly_two_cost(n: Node) -> SymbolicCost { } } -fn r1_acc_direct_in_copied_port( - acc: Symbol, - combiner: Symbol, - port0: Symbol, - port1: Symbol -) -> Bool { - match r1_copied_port_index(combiner: combiner) { - Present { value: copied_idx } => - if copied_idx == 0 { - r1_symbols_equal(a: acc, b: port0) - } else { - r1_symbols_equal(a: acc, b: port1) - } - Absent => false - } +fn r1_some_finding(f: Finding) -> Optional { + Present { value: f } } -fn r1_acc_visible_in_call(acc: Symbol, port0: Symbol, port1: Symbol) -> Bool { - r1_symbols_equal(a: acc, b: port0) || r1_symbols_equal(a: acc, b: port1) -} - -fn r1_fold_step_subject( - acc_binder: Symbol, +fn classify_call( + at: Node, combiner: Symbol, - port0_arg: Symbol, - port1_arg: Symbol -) -> Node { - Node { - kind: TypeNode { connective: Instantiation }, - children: [ - Edge { label: Positional, target: r1_symbol_atom(s: acc_binder) }, - Edge { label: Positional, target: r1_symbol_atom(s: combiner) }, - Edge { - label: Positional, - target: Node { - kind: TypeNode { connective: Instantiation }, - children: [ - Edge { label: Positional, target: r1_symbol_atom(s: port0_arg) }, - Edge { label: Positional, target: r1_symbol_atom(s: port1_arg) } - ], - occurrence_id: SyntheticOccurrence - } - } - ], - occurrence_id: SyntheticOccurrence - } -} - -fn r1_judge_fold_step(n: Node) -> R1JudgeResult { - let positions = r1_positional_targets(n: n) - match list_at_optional(xs: positions, index: 0) { - Absent => R1MalformedSubject - Present { value: acc_node } => - match r1_symbol_of(n: acc_node) { - Absent => R1MalformedSubject - Present { value: acc } => - match list_at_optional(xs: positions, index: 1) { - Absent => R1MalformedSubject - Present { value: combiner_node } => - match r1_symbol_of(n: combiner_node) { - Absent => R1MalformedSubject - Present { value: combiner } => - match list_at_optional(xs: positions, index: 2) { - Absent => R1Clean { flow_opaque_count: 0 } - Present { value: call_node } => - let call_ports = r1_positional_targets(n: call_node) - match list_at_optional(xs: call_ports, index: 0) { - Absent => R1Clean { flow_opaque_count: 0 } - Present { value: p0_node } => - match r1_symbol_of(n: p0_node) { - Absent => R1Clean { flow_opaque_count: 1 } - Present { value: port0 } => - match list_at_optional(xs: call_ports, index: 1) { - Absent => R1Clean { flow_opaque_count: 1 } - Present { value: p1_node } => - match r1_symbol_of(n: p1_node) { - Absent => R1Clean { flow_opaque_count: 1 } - Present { value: port1 } => - if r1_acc_direct_in_copied_port( - acc: acc, - combiner: combiner, - port0: port0, - port1: port1 - ) { - R1PolyTwoSuspect { - implied_cost: r1_poly_two_cost(n: n), - flow_opaque_count: 0 - } - } else { - if r1_acc_visible_in_call( - acc: acc, - port0: port0, - port1: port1 - ) { - R1Clean { flow_opaque_count: 0 } - } else { - R1Clean { flow_opaque_count: 1 } - } - } - } - } - } - } - } + port_syms: List>, + carriers: List +) -> Optional { + match r1_copied_port_index(combiner: combiner) { + Absent => Absent + Present { value: idx } => + match list_at_optional(xs: port_syms, index: idx) { + Absent => Absent + Present { value: copied } => + match copied { + Present { value: p } => + if symbol_in(needle: p, xs: carriers) { + r1_some_finding(f: Poly2Suspect { at: at, cost: r1_poly_two_cost(n: at) }) + } else { + Absent } + Absent => + r1_some_finding(f: AnalysisOpaque { at: at, reason: ^r1_copied_port_opaque }) } } } } -fn complexity_r1_flow_opaque_diagnostic() -> Diagnostic { - Diagnostic { - reason: ^complexity_r1_flow_opaque_residue, - at: Textual { file: ^complexity_r1_lens_virtual_file, extent: WholeFile }, - correction: Unavailable { reason: ExternalContractUnknown } - } -} - -fn complexity_r1_malformed_subject_diagnostic() -> Diagnostic { - Diagnostic { - reason: ^complexity_r1_malformed_fold_step_subject, - at: Textual { file: ^complexity_r1_lens_virtual_file, extent: WholeFile }, - correction: Unavailable { reason: ExternalContractUnknown } - } -} - -fn complexity_r1_accumulator_copy_lens(n: Node) -> Witness { - match r1_judge_fold_step(n: n) { - R1PolyTwoSuspect { implied_cost: cost, flow_opaque_count: _ } => - Holds { value: cost } - R1Clean { flow_opaque_count: 0 } => - Holds { value: zero_cost() } - R1Clean { flow_opaque_count: _ } => - Violates { diagnostic: complexity_r1_flow_opaque_diagnostic() } - R1MalformedSubject => - Violates { diagnostic: complexity_r1_malformed_subject_diagnostic() } - } -} - data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { dissolves_to: SubstrateMandatoryTag } } diff --git a/src/v2/lens/complexity_r1_accumulator_copy/analyze.dag b/src/v2/lens/complexity_r1_accumulator_copy/analyze.dag new file mode 100644 index 00000000000..f6b7cd0fe1f --- /dev/null +++ b/src/v2/lens/complexity_r1_accumulator_copy/analyze.dag @@ -0,0 +1,203 @@ +module v2.lens.complexity_r1_accumulator_copy.analyze + +import v2.lens.complexity_r1_accumulator_copy { + AnalysisOpaque, + Finding, + Poly2Suspect, + classify_call +} +import v2.extdeps.languages.dag { + ParseSubtreeAbsent, + ParseSubtreeFound, + parse_production_captured_child_optional, + parse_production_emitted_identity_optional, + parse_subtree_find_production_captured +} +import std.algebra { Cons, Empty } +import v2.std.algebra { list_append, list_snoc_item } +import v2.std.collection { Absent, List, Optional, Present } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.grammar { node_atom_identity_optional } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.node_query { find_named_child } + +data analyze_note: String = "The TRAVERSAL half of the R1 accumulator-copy lens — the linear fold that replaces the deleted surface-navigation bridge. analyze(node, carriers) is one recursion over the whole Node tree threading a carrier environment DOWN: at a fold-family call it binds the step function's accumulator (its first param); at every combiner call it asks the cost model (classify_call) whether a bound carrier sits in that combiner's copied port. Because it VISITS every node rather than doing targeted lookup, a copy inside an if/match/let is found by construction — the whole class of control-flow shape gaps the old bridge had dissolves. Three reads here are still surface/syntactic guesses (the subject of the follow-on discussion): the carrier is the step-fn's positional first param; the combiner is matched by lexeme name; carrier-in-copied-port is symbol equality, not dataflow — so a carrier renamed through a let, or a combiner shadowed, is not yet followed. Ports are read as DIRECT args (collect_direct_captures does not descend into an arg's value) so a nested call in one argument does not shift the copied-port index (map_merge's copied port is index 1)." + +fn named_child_optional(cap: Node, name: Symbol) -> Optional { + match find_named_child(root: cap, name: name) { + Accepted { value: c, diagnostics: _ } => Present { value: c } + Rejected { diagnostics: _ } => Absent + } +} + +fn sequence_left_node(cap: Node) -> Optional { + named_child_optional(cap: cap, name: ^grammar_sequence_left_node_projection) +} + +fn sequence_right_node(cap: Node) -> Optional { + named_child_optional(cap: cap, name: ^grammar_sequence_right_node_projection) +} + +fn sequence_left_symbol(cap: Node) -> Optional { + match sequence_left_node(cap: cap) { + Absent => Absent + Present { value: left } => node_atom_identity_optional(node: left) + } +} + +fn find_capture(root: Node, emitted: Symbol) -> Optional { + match parse_subtree_find_production_captured(root: root, emitted: emitted) { + ParseSubtreeFound { captured: c } => Present { value: c } + ParseSubtreeAbsent => Absent + } +} + +fn collect_direct_captures(n: Node, emitted: Symbol, acc: List) -> List { + match parse_production_emitted_identity_optional(node: n) { + Present { value: id } => + if id == emitted { + match parse_production_captured_child_optional(node: n) { + Present { value: c } => list_snoc_item(xs: acc, item: c) + Absent => acc + } + } else { + fold(n.children, init: acc, f: fn(a, e) { + collect_direct_captures(n: e.target, emitted: emitted, acc: a) + }) + } + Absent => + fold(n.children, init: acc, f: fn(a, e) { + collect_direct_captures(n: e.target, emitted: emitted, acc: a) + }) + } +} + +fn primary_expr_capture(node: Node) -> Optional { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => + if id == ^dag_surface_primary_expr { + parse_production_captured_child_optional(node: node) + } else { + Absent + } + Absent => Absent + } +} + +fn arg_value_symbol(arg_capture: Node) -> Optional { + match find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) { + Absent => Absent + Present { value: value_expr } => sequence_left_symbol(cap: value_expr) + } +} + +fn call_port_symbols(call_capture: Node) -> List> { + fold( + collect_direct_captures(n: call_capture, emitted: ^dag_surface_arg, acc: Empty), + init: Empty, + f: fn(acc, arg) { list_snoc_item(xs: acc, item: arg_value_symbol(arg_capture: arg)) } + ) +} + +fn is_fold_family_head(sym: Symbol) -> Bool { + (sym == ^fold) || (sym == ^fold_list) || (sym == ^fold_node) +} + +fn step_fn_first_param(fn_literal: Node) -> Optional { + match sequence_right_node(cap: fn_literal) { + Absent => Absent + Present { value: after_kw_fn } => + match sequence_right_node(cap: after_kw_fn) { + Absent => Absent + Present { value: after_lparen } => + match sequence_left_node(cap: after_lparen) { + Absent => Absent + Present { value: params } => sequence_left_symbol(cap: params) + } + } + } +} + +fn fold_family_carrier(call_capture: Node) -> Optional { + match sequence_left_symbol(cap: call_capture) { + Absent => Absent + Present { value: head } => + if is_fold_family_head(sym: head) { + match find_capture(root: call_capture, emitted: ^dag_surface_fn_literal) { + Absent => Absent + Present { value: fn_literal } => step_fn_first_param(fn_literal: fn_literal) + } + } else { + Absent + } + } +} + +fn extend_carriers(call_capture: Node, carriers: List) -> List { + match fold_family_carrier(call_capture: call_capture) { + Present { value: carrier } => Cons { head: carrier, tail: carriers } + Absent => carriers + } +} + +fn finding_at_call(node: Node, call_capture: Node, carriers: List) -> List { + match sequence_left_symbol(cap: call_capture) { + Absent => Empty + Present { value: combiner } => + match classify_call( + at: node, + combiner: combiner, + port_syms: call_port_symbols(call_capture: call_capture), + carriers: carriers + ) { + Present { value: f } => Cons { head: f, tail: Empty } + Absent => Empty + } + } +} + +fn analyze(node: Node, carriers: List) -> List { + match primary_expr_capture(node: node) { + Absent => + fold(node.children, init: Empty, f: fn(acc, e) { + list_append(left: acc, right: analyze(node: e.target, carriers: carriers)) + }) + Present { value: cap } => + let carriers2 = extend_carriers(call_capture: cap, carriers: carriers) + let here = finding_at_call(node: node, call_capture: cap, carriers: carriers2) + fold(node.children, init: here, f: fn(acc, e) { + list_append(left: acc, right: analyze(node: e.target, carriers: carriers2)) + }) + } +} + +fn r1_findings(root: Node) -> List { + analyze(node: root, carriers: Empty) +} + +fn finding_is_suspect(f: Finding) -> Bool { + match f { + Poly2Suspect { at: _, cost: _ } => true + AnalysisOpaque { at: _, reason: _ } => false + } +} + +fn finding_is_opaque(f: Finding) -> Bool { + match f { + Poly2Suspect { at: _, cost: _ } => false + AnalysisOpaque { at: _, reason: _ } => true + } +} + +fn findings_any(fs: List, pred: fn(Finding) -> Bool) -> Bool { + fold(fs, init: false, f: fn(acc, x) { if acc { true } else { pred(x) } }) +} + +fn findings_have_suspect(fs: List) -> Bool { + findings_any(fs: fs, pred: finding_is_suspect) +} + +fn findings_have_opaque(fs: List) -> Bool { + findings_any(fs: fs, pred: finding_is_opaque) +} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/green_cons_prepend.dag b/src/v2/lens/complexity_r1_accumulator_copy/green_cons_prepend.dag deleted file mode 100644 index 9844254061c..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/green_cons_prepend.dag +++ /dev/null @@ -1,55 +0,0 @@ -module v2.test.lens_complexity_r1_accumulator_copy.green_cons_prepend - -import v2.lens.complexity_r1_accumulator_copy { - R1Clean, - r1_fold_step_subject, - r1_judge_fold_step -} -import v2.std.logic { Bool } -import v2.std.node { Conj, Node, SyntheticOccurrence, Symbol, TypeNode } -import v2.std.verification { - EqualsClaim, - TestClaim, - TestClassification, - ManualAnchorAbsent, - Tier1, - Unit, - manual_claim_anchor -} - -data r1_prepend_acc: Symbol = ^r1_prepend_acc -data r1_prepend_head: Symbol = ^r1_prepend_head - -data green_cons_prepend_input: Node = r1_fold_step_subject( - acc_binder: r1_prepend_acc, - combiner: ^Cons, - port0_arg: r1_prepend_head, - port1_arg: r1_prepend_acc -) - -fn green_cons_prepend_claim_holds() -> Bool { - match r1_judge_fold_step(n: green_cons_prepend_input) { - R1Clean { flow_opaque_count: 0 } => true - _ => false - } -} - -fn green_cons_prepend_claim_rhs() -> Node { - if green_cons_prepend_claim_holds() { - green_cons_prepend_input - } else { - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - -data claim_green_cons_prepend: TestClaim = EqualsClaim { - label: "lens_complexity_r1/green_cons_prepend: Cons { head, tail: acc } fold step is not R1", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: green_cons_prepend_input, - rhs: green_cons_prepend_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/green_merge_envs_base_acc.dag b/src/v2/lens/complexity_r1_accumulator_copy/green_merge_envs_base_acc.dag deleted file mode 100644 index f74f78c2e4a..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/green_merge_envs_base_acc.dag +++ /dev/null @@ -1,55 +0,0 @@ -module v2.test.lens_complexity_r1_accumulator_copy.green_merge_envs_base_acc - -import v2.lens.complexity_r1_accumulator_copy { - R1Clean, - r1_fold_step_subject, - r1_judge_fold_step -} -import v2.std.logic { Bool } -import v2.std.node { Conj, Node, SyntheticOccurrence, Symbol, TypeNode } -import v2.std.verification { - EqualsClaim, - TestClaim, - TestClassification, - ManualAnchorAbsent, - Tier1, - Unit, - manual_claim_anchor -} - -data r1_merge_acc: Symbol = ^r1_merge_acc -data r1_merge_chunk: Symbol = ^r1_merge_chunk - -data green_merge_envs_base_acc_input: Node = r1_fold_step_subject( - acc_binder: r1_merge_acc, - combiner: ^map_merge, - port0_arg: r1_merge_acc, - port1_arg: r1_merge_chunk -) - -fn green_merge_envs_base_acc_claim_holds() -> Bool { - match r1_judge_fold_step(n: green_merge_envs_base_acc_input) { - R1Clean { flow_opaque_count: 0 } => true - _ => false - } -} - -fn green_merge_envs_base_acc_claim_rhs() -> Node { - if green_merge_envs_base_acc_claim_holds() { - green_merge_envs_base_acc_input - } else { - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - -data claim_green_merge_envs_base_acc: TestClaim = EqualsClaim { - label: "lens_complexity_r1/green_merge_envs_base_acc: acc in map_merge base port is not R1 (shape formerly live as merge_envs, deleted from src/v1/04_env.dag 2026-07-06)", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: green_merge_envs_base_acc_input, - rhs: green_merge_envs_base_acc_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/red_compositional_env_union.dag b/src/v2/lens/complexity_r1_accumulator_copy/red_compositional_env_union.dag deleted file mode 100644 index f124b8e5f5b..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/red_compositional_env_union.dag +++ /dev/null @@ -1,55 +0,0 @@ -module v2.test.lens_complexity_r1_accumulator_copy.red_compositional_env_union - -import v2.lens.complexity_r1_accumulator_copy { - R1PolyTwoSuspect, - r1_fold_step_subject, - r1_judge_fold_step -} -import v2.std.logic { Bool } -import v2.std.node { Conj, Node, SyntheticOccurrence, Symbol, TypeNode } -import v2.std.verification { - EqualsClaim, - TestClaim, - TestClassification, - ManualAnchorAbsent, - Tier1, - Unit, - manual_claim_anchor -} - -data r1_union_acc: Symbol = ^r1_union_acc -data r1_union_delta: Symbol = ^r1_union_delta - -data red_compositional_env_union_input: Node = r1_fold_step_subject( - acc_binder: r1_union_acc, - combiner: ^map_merge, - port0_arg: r1_union_delta, - port1_arg: r1_union_acc -) - -fn red_compositional_env_union_claim_holds() -> Bool { - match r1_judge_fold_step(n: red_compositional_env_union_input) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - _ => false - } -} - -fn red_compositional_env_union_claim_rhs() -> Node { - if red_compositional_env_union_claim_holds() { - red_compositional_env_union_input - } else { - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - -data claim_red_compositional_env_union: TestClaim = EqualsClaim { - label: "lens_complexity_r1/red_compositional_env_union: small-delta base + acc overlay still hits map_merge overlay copied-port", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: red_compositional_env_union_input, - rhs: red_compositional_env_union_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/red_list_append_left.dag b/src/v2/lens/complexity_r1_accumulator_copy/red_list_append_left.dag deleted file mode 100644 index 27d6d680f25..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/red_list_append_left.dag +++ /dev/null @@ -1,55 +0,0 @@ -module v2.test.lens_complexity_r1_accumulator_copy.red_list_append_left - -import v2.lens.complexity_r1_accumulator_copy { - R1PolyTwoSuspect, - r1_fold_step_subject, - r1_judge_fold_step -} -import v2.std.logic { Bool } -import v2.std.node { Conj, Node, SyntheticOccurrence, Symbol, TypeNode } -import v2.std.verification { - EqualsClaim, - TestClaim, - TestClassification, - ManualAnchorAbsent, - Tier1, - Unit, - manual_claim_anchor -} - -data r1_red_acc: Symbol = ^r1_red_acc -data r1_red_item: Symbol = ^r1_red_item - -data red_list_append_left_input: Node = r1_fold_step_subject( - acc_binder: r1_red_acc, - combiner: ^list_append, - port0_arg: r1_red_acc, - port1_arg: r1_red_item -) - -fn red_list_append_left_claim_holds() -> Bool { - match r1_judge_fold_step(n: red_list_append_left_input) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - _ => false - } -} - -fn red_list_append_left_claim_rhs() -> Node { - if red_list_append_left_claim_holds() { - red_list_append_left_input - } else { - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - -data claim_red_list_append_left: TestClaim = EqualsClaim { - label: "lens_complexity_r1/red_list_append_left: glob_discovery_law.dag:63 shape (list_append left:acc) projects Poly(2)", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: red_list_append_left_input, - rhs: red_list_append_left_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/red_map_merge_overlay_acc.dag b/src/v2/lens/complexity_r1_accumulator_copy/red_map_merge_overlay_acc.dag deleted file mode 100644 index 7115cbe7f4a..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/red_map_merge_overlay_acc.dag +++ /dev/null @@ -1,55 +0,0 @@ -module v2.test.lens_complexity_r1_accumulator_copy.red_map_merge_overlay_acc - -import v2.lens.complexity_r1_accumulator_copy { - R1PolyTwoSuspect, - r1_fold_step_subject, - r1_judge_fold_step -} -import v2.std.logic { Bool } -import v2.std.node { Conj, Node, SyntheticOccurrence, Symbol, TypeNode } -import v2.std.verification { - EqualsClaim, - TestClaim, - TestClassification, - ManualAnchorAbsent, - Tier1, - Unit, - manual_claim_anchor -} - -data r1_red_acc: Symbol = ^r1_red_acc -data r1_red_chunk: Symbol = ^r1_red_chunk - -data red_map_merge_overlay_acc_input: Node = r1_fold_step_subject( - acc_binder: r1_red_acc, - combiner: ^map_merge, - port0_arg: r1_red_chunk, - port1_arg: r1_red_acc -) - -fn red_map_merge_overlay_acc_claim_holds() -> Bool { - match r1_judge_fold_step(n: red_map_merge_overlay_acc_input) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - _ => false - } -} - -fn red_map_merge_overlay_acc_claim_rhs() -> Node { - if red_map_merge_overlay_acc_claim_holds() { - red_map_merge_overlay_acc_input - } else { - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - -data claim_red_map_merge_overlay_acc: TestClaim = EqualsClaim { - label: "lens_complexity_r1/red_map_merge_overlay_acc: acc in map_merge overlay port (v1_rt.rs:360 copied-port) fires Poly(2)", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: red_map_merge_overlay_acc_input, - rhs: red_map_merge_overlay_acc_claim_rhs(), - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag b/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag deleted file mode 100644 index 6de55105630..00000000000 --- a/src/v2/lens/complexity_r1_accumulator_copy/surface_subject.dag +++ /dev/null @@ -1,209 +0,0 @@ -module v2.lens.complexity_r1_accumulator_copy.surface_subject - -import v2.compiler.fold_lowering { fold_call_step_fn } -import v2.lens.complexity_r1_accumulator_copy { r1_fold_step_subject } -import v2.extdeps.languages.dag { - ParseSubtreeAbsent, - ParseSubtreeFound, - parse_production_captured_child_optional, - parse_production_emitted_identity_optional, - parse_subtree_find_production_captured -} -import std.algebra { Empty } -import v2.std.algebra { list_snoc_item } -import v2.std.collection { Absent, List, Optional, Present, list_at_optional } -import v2.std.diagnostic { - Accepted, - Diagnostic, - ExternalContractUnknown, - Outcome, - Rejected, - Unavailable, - node_locus, - outcome_accepted, - outcome_rejected -} -import v2.std.grammar { node_atom_identity_optional } -import v2.std.integer { Int } -import v2.std.node { Node, Symbol } -import v2.std.node_query { find_named_child } - -data surface_subject_note: String = "Distills a real surface fold call into the R1 accumulator-copy lens's fold-step subject (Instantiation[acc_binder, combiner, call[port0, port1]]) — the peer projection of v2.compiler.fold_lowering.fold_call_to_loop (§2 Realization: one surface fold call, N consumers — the loop projection is for termination, this one is for cost/copy-detection). It reads the SAME located fold call through the SAME fn-literal locator (fold_call_step_fn), then reads four symbols at the surface/lexeme level (post the StampLexeme grammar fixes, so both param decls and call heads carry their names): acc_binder = the step function's FIRST param (the fold accumulator); combiner = the head of the call in the step-fn body; port0/port1 = that call's first two argument values, in declared order. R1 then judges whether acc_binder lands in the combiner's copied port (copied_port_fact_registry). Fail-closed: any missing piece (no step fn, no first param, body is not a two-argument call, an argument value is not a bare name) REFUSES with a located diagnostic — never fabricates a subject, so a fold R1 cannot read never silently reads as clean. This is surface-level (pre-resolve) because corpus resolution/body-production is not yet affordable; when it is, the resolved-body read supersedes this and the seam (fold_call_step_fn) is unchanged. Verified end-to-end on real source (v2.test.claim.complexity.r1_surface_subject): list_append(left: acc, …) projects Poly(2); list_append(right: acc) with acc out of the copied port is clean — same combiner, accumulator position flipped, isolating the copied-port check." - -fn named_child_optional(cap: Node, name: Symbol) -> Optional { - match find_named_child(root: cap, name: name) { - Accepted { value: c, diagnostics: _ } => Present { value: c } - Rejected { diagnostics: _ } => Absent - } -} - -fn sequence_left_node(cap: Node) -> Optional { - named_child_optional(cap: cap, name: ^grammar_sequence_left_node_projection) -} - -fn sequence_right_node(cap: Node) -> Optional { - named_child_optional(cap: cap, name: ^grammar_sequence_right_node_projection) -} - -fn sequence_left_symbol(cap: Node) -> Optional { - match sequence_left_node(cap: cap) { - Absent => Absent - Present { value: left } => node_atom_identity_optional(node: left) - } -} - -fn find_capture(root: Node, emitted: Symbol) -> Optional { - match parse_subtree_find_production_captured(root: root, emitted: emitted) { - ParseSubtreeFound { captured: c } => Present { value: c } - ParseSubtreeAbsent => Absent - } -} - -fn collect_captures(n: Node, emitted: Symbol, acc: List) -> List { - let acc1 = match parse_production_emitted_identity_optional(node: n) { - Present { value: id } => - if id == emitted { - match parse_production_captured_child_optional(node: n) { - Present { value: c } => list_snoc_item(xs: acc, item: c) - Absent => acc - } - } else { - acc - } - Absent => acc - } - fold(n.children, init: acc1, f: fn(a, e) { - collect_captures(n: e.target, emitted: emitted, acc: a) - }) -} - -fn step_fn_first_param_symbol(fn_literal: Node) -> Optional { - match sequence_right_node(cap: fn_literal) { - Absent => Absent - Present { value: after_kw_fn } => - match sequence_right_node(cap: after_kw_fn) { - Absent => Absent - Present { value: after_lparen } => - match sequence_left_node(cap: after_lparen) { - Absent => Absent - Present { value: params } => sequence_left_symbol(cap: params) - } - } - } -} - -fn step_fn_body_call(fn_literal: Node) -> Optional { - match find_capture(root: fn_literal, emitted: ^dag_surface_fn_body) { - Absent => Absent - Present { value: body } => find_capture(root: body, emitted: ^dag_surface_primary_expr) - } -} - -fn body_call_combiner_symbol(body_call: Node) -> Optional { - sequence_left_symbol(cap: body_call) -} - -fn arg_value_symbol(arg_capture: Node) -> Optional { - match find_capture(root: arg_capture, emitted: ^dag_surface_primary_expr) { - Absent => Absent - Present { value: value_expr } => sequence_left_symbol(cap: value_expr) - } -} - -fn body_call_port_symbol(body_call: Node, index: Int) -> Optional { - match list_at_optional( - xs: collect_captures(n: body_call, emitted: ^dag_surface_arg, acc: Empty), - index: index - ) { - Absent => Absent - Present { value: arg } => arg_value_symbol(arg_capture: arg) - } -} - -type FoldSurfaceRead - = FoldSurfaceSubject { subject: Node } - | FoldSurfaceNoStepFn - | FoldSurfaceNoAccumulatorParam - | FoldSurfaceBodyNotLocated - | FoldSurfaceBodyHeadOpaque - | FoldSurfacePort0Opaque - | FoldSurfacePort1Opaque - -fn read_fold_surface(fold_call: Node) -> FoldSurfaceRead { - match fold_call_step_fn(fold_call: fold_call) { - Absent => FoldSurfaceNoStepFn - Present { value: fn_literal } => - match step_fn_first_param_symbol(fn_literal: fn_literal) { - Absent => FoldSurfaceNoAccumulatorParam - Present { value: acc_binder } => - match step_fn_body_call(fn_literal: fn_literal) { - Absent => FoldSurfaceBodyNotLocated - Present { value: body_call } => - match body_call_combiner_symbol(body_call: body_call) { - Absent => FoldSurfaceBodyHeadOpaque - Present { value: combiner } => - match body_call_port_symbol(body_call: body_call, index: 0) { - Absent => FoldSurfacePort0Opaque - Present { value: port0 } => - match body_call_port_symbol(body_call: body_call, index: 1) { - Absent => FoldSurfacePort1Opaque - Present { value: port1 } => - FoldSurfaceSubject { - subject: r1_fold_step_subject( - acc_binder: acc_binder, - combiner: combiner, - port0_arg: port0, - port1_arg: port1 - ) - } - } - } - } - } - } - } -} - -fn fold_surface_refusal_reason(read: FoldSurfaceRead) -> Symbol { - match read { - FoldSurfaceSubject { subject: _ } => ^r1_surface_subject_present - FoldSurfaceNoStepFn => ^r1_surface_no_step_fn - FoldSurfaceNoAccumulatorParam => ^r1_surface_no_accumulator_param - FoldSurfaceBodyNotLocated => ^r1_surface_body_not_located - FoldSurfaceBodyHeadOpaque => ^r1_surface_body_head_opaque - FoldSurfacePort0Opaque => ^r1_surface_port0_opaque - FoldSurfacePort1Opaque => ^r1_surface_port1_opaque - } -} - -fn surface_subject_diagnostic(reason: Symbol, n: Node) -> Diagnostic { - Diagnostic { - reason: reason, - at: node_locus(node: n), - correction: Unavailable { reason: ExternalContractUnknown } - } -} - -fn fold_call_to_r1_subject(fold_call: Node) -> Outcome { - match read_fold_surface(fold_call: fold_call) { - FoldSurfaceSubject { subject: subject } => outcome_accepted(value: subject) - FoldSurfaceNoStepFn => - outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_no_step_fn, n: fold_call)) - FoldSurfaceNoAccumulatorParam => - outcome_rejected( - d: surface_subject_diagnostic(reason: ^r1_surface_no_accumulator_param, n: fold_call) - ) - FoldSurfaceBodyNotLocated => - outcome_rejected( - d: surface_subject_diagnostic(reason: ^r1_surface_body_not_located, n: fold_call) - ) - FoldSurfaceBodyHeadOpaque => - outcome_rejected( - d: surface_subject_diagnostic(reason: ^r1_surface_body_head_opaque, n: fold_call) - ) - FoldSurfacePort0Opaque => - outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_port0_opaque, n: fold_call)) - FoldSurfacePort1Opaque => - outcome_rejected(d: surface_subject_diagnostic(reason: ^r1_surface_port1_opaque, n: fold_call)) - } -} diff --git a/src/v2/lens/complexity_r1_accumulator_copy_test.dag b/src/v2/lens/complexity_r1_accumulator_copy_test.dag index 94c217bf47e..849eeb3a85f 100644 --- a/src/v2/lens/complexity_r1_accumulator_copy_test.dag +++ b/src/v2/lens/complexity_r1_accumulator_copy_test.dag @@ -1,56 +1,128 @@ module v2.test.lens_complexity_r1_accumulator_copy import v2.lens.complexity_r1_accumulator_copy { - R1Clean, - R1PolyTwoSuspect, - r1_fold_step_subject, - r1_judge_fold_step + AnalysisOpaque, + Finding, + Poly2Suspect, + classify_call } +import v2.std.collection { Absent, List, Optional, Present } import v2.std.logic { Bool } -import v2.std.node { Symbol } +import v2.std.node { Atom, Node, Symbol, SyntheticOccurrence, TypeNode } -data r1_hygiene_acc: Symbol = ^r1_hygiene_acc -data r1_hygiene_item: Symbol = ^r1_hygiene_item -data r1_hygiene_chunk: Symbol = ^r1_hygiene_chunk +data r1_cost_model_note: String = "Unit-tests the COST MODEL (classify_call) directly against the copied-port registry — no fold, no ingest, no intermediate subject. Each row asserts the verdict for a synthetic (combiner, ports, carriers): the accumulator in a copied port is a Poly(2) suspect (list_append/list_snoc copied index 0, map_merge copied index 1); the accumulator in a NON-copied port is Absent (clean); an unregistered combiner is Absent; a copied port that is not a bare name is AnalysisOpaque (fail-closed, counted — never silently clean)." -test fn complexity_r1_red_list_append_left_holds() -> Bool { - match r1_judge_fold_step( - n: r1_fold_step_subject( - acc_binder: r1_hygiene_acc, +fn r1_dummy() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: ^r1_dummy } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn present(s: Symbol) -> Optional { + Present { value: s } +} + +fn classify(combiner: Symbol, port_syms: List>, carriers: List) -> Optional { + classify_call(at: r1_dummy(), combiner: combiner, port_syms: port_syms, carriers: carriers) +} + +fn is_suspect(o: Optional) -> Bool { + match o { + Present { value: f } => + match f { + Poly2Suspect { at: _, cost: _ } => true + AnalysisOpaque { at: _, reason: _ } => false + } + Absent => false + } +} + +fn is_opaque(o: Optional) -> Bool { + match o { + Present { value: f } => + match f { + Poly2Suspect { at: _, cost: _ } => false + AnalysisOpaque { at: _, reason: _ } => true + } + Absent => false + } +} + +fn is_absent(o: Optional) -> Bool { + match o { + Present { value: _ } => false + Absent => true + } +} + +test fn red_list_append_left_is_suspect() -> Bool { + is_suspect( + o: classify( combiner: ^list_append, - port0_arg: r1_hygiene_acc, - port1_arg: r1_hygiene_item + port_syms: [present(s: ^acc), present(s: ^item)], + carriers: [^acc] ) - ) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - _ => false - } + ) } -test fn complexity_r1_green_merge_envs_base_holds() -> Bool { - match r1_judge_fold_step( - n: r1_fold_step_subject( - acc_binder: r1_hygiene_acc, +test fn red_list_snoc_left_is_suspect() -> Bool { + is_suspect( + o: classify( + combiner: ^list_snoc_item, + port_syms: [present(s: ^acc), present(s: ^item)], + carriers: [^acc] + ) + ) +} + +test fn red_map_merge_overlay_is_suspect() -> Bool { + is_suspect( + o: classify( combiner: ^map_merge, - port0_arg: r1_hygiene_acc, - port1_arg: r1_hygiene_chunk + port_syms: [present(s: ^base), present(s: ^acc)], + carriers: [^acc] ) - ) { - R1Clean { flow_opaque_count: 0 } => true - _ => false - } + ) } -test fn complexity_r1_red_map_merge_overlay_holds() -> Bool { - match r1_judge_fold_step( - n: r1_fold_step_subject( - acc_binder: r1_hygiene_acc, +test fn green_map_merge_base_is_clean() -> Bool { + is_absent( + o: classify( combiner: ^map_merge, - port0_arg: r1_hygiene_chunk, - port1_arg: r1_hygiene_acc + port_syms: [present(s: ^acc), present(s: ^other)], + carriers: [^acc] ) - ) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - _ => false - } + ) +} + +test fn green_list_append_acc_in_noncopied_port_is_clean() -> Bool { + is_absent( + o: classify( + combiner: ^list_append, + port_syms: [present(s: ^item), present(s: ^acc)], + carriers: [^acc] + ) + ) +} + +test fn green_unregistered_combiner_is_clean() -> Bool { + is_absent( + o: classify( + combiner: ^Cons, + port_syms: [present(s: ^item), present(s: ^acc)], + carriers: [^acc] + ) + ) +} + +test fn opaque_copied_port_is_analysis_opaque() -> Bool { + is_opaque( + o: classify( + combiner: ^list_append, + port_syms: [Absent, present(s: ^item)], + carriers: [^acc] + ) + ) } diff --git a/src/v2/test/claim/complexity/r1_fold_analysis_test.dag b/src/v2/test/claim/complexity/r1_fold_analysis_test.dag new file mode 100644 index 00000000000..f57b7a2fe35 --- /dev/null +++ b/src/v2/test/claim/complexity/r1_fold_analysis_test.dag @@ -0,0 +1,84 @@ +module v2.test.claim.complexity.r1_fold_analysis + +import v2.compiler.normalize { normalize } +import v2.compiler.parse { parse_module } +import v2.compiler.tokenize { tokenize } +import v2.lens.complexity_r1_accumulator_copy { Finding } +import v2.lens.complexity_r1_accumulator_copy.analyze { + findings_have_opaque, + findings_have_suspect, + r1_findings +} +import v2.extdeps.languages.dag { dag_language_model_wave1 } +import v2.std.collection { Absent, List, Optional, Present } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.text { String } + +data r1_fold_analysis_note: String = "Drives the linear R1 fold (v2.lens.complexity_r1_accumulator_copy.analyze.r1_findings) end-to-end on real source through the census ingest (tokenize/parse/normalize) — no distiller bridge, no intermediate subject. The fold visits every node and threads the carrier, so the checks are: a direct copied-port fold projects a Poly(2) suspect; the SAME combiner with the accumulator flipped to the non-copied port is clean; an identity-body fold yields nothing (no combiner site); and — the coverage win the bridge could not reach — the real glob_discovery_law shape (fold_list with the copying list_append(left: acc, ...) buried inside an if-branch and a grow-by-one struct arg) is now CAUGHT, because the fold visits the copy inside the branch rather than reading the branch condition." + +data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" + +data linear_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" + +data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" + +data real_branch_body_snippet: String = "module rs\n\nfn g(xs: List) -> Int {\n fold_list(xs: xs, empty: Empty, cons: fn(acc, r) {\n if pred(r: r) {\n list_append(left: acc, right: Cons { head: r, tail: Empty })\n } else {\n acc\n }\n })\n}\n" + +fn ingest(source_text: String, file: Symbol) -> Optional { + let lm = dag_language_model_wave1() + match tokenize(text: source_text, file: file, rules: lm.lex) { + Rejected { diagnostics: _ } => Absent + Accepted { value: ts, diagnostics: _ } => + match parse_module(tokens: ts, grammar: lm.grammar) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => + match normalize(parse_tree: artifact.tree) { + Rejected { diagnostics: _ } => Absent + Accepted { value: tree, diagnostics: _ } => Present { value: tree } + } + } + } +} + +fn findings_of(source_text: String, file: Symbol) -> Optional> { + match ingest(source_text: source_text, file: file) { + Absent => Absent + Present { value: tree } => Present { value: r1_findings(root: tree) } + } +} + +test fn quadratic_fold_has_suspect() -> Bool { + match findings_of(source_text: quadratic_snippet, file: ^quad_file) { + Absent => false + Present { value: fs } => findings_have_suspect(fs: fs) + } +} + +test fn linear_fold_has_no_suspect() -> Bool { + match findings_of(source_text: linear_snippet, file: ^lin_file) { + Absent => false + Present { value: fs } => + if findings_have_suspect(fs: fs) { false } else { true } + } +} + +test fn identity_fold_has_no_finding() -> Bool { + match findings_of(source_text: identity_snippet, file: ^ident_file) { + Absent => false + Present { value: fs } => + if findings_have_suspect(fs: fs) { + false + } else { + if findings_have_opaque(fs: fs) { false } else { true } + } + } +} + +test fn real_branch_body_quadratic_is_caught() -> Bool { + match findings_of(source_text: real_branch_body_snippet, file: ^rs_file) { + Absent => false + Present { value: fs } => findings_have_suspect(fs: fs) + } +} diff --git a/src/v2/test/claim/complexity/r1_surface_subject_test.dag b/src/v2/test/claim/complexity/r1_surface_subject_test.dag deleted file mode 100644 index d12558c4d46..00000000000 --- a/src/v2/test/claim/complexity/r1_surface_subject_test.dag +++ /dev/null @@ -1,126 +0,0 @@ -module v2.test.claim.complexity.r1_surface_subject - -import v2.compiler.normalize { normalize } -import v2.compiler.parse { parse_module } -import v2.compiler.tokenize { tokenize } -import v2.lens.complexity_r1_accumulator_copy { - R1Clean, - R1MalformedSubject, - R1PolyTwoSuspect, - r1_judge_fold_step -} -import v2.lens.complexity_r1_accumulator_copy.surface_subject { fold_call_to_r1_subject } -import v2.extdeps.languages.dag { - ParseSubtreeAbsent, - ParseSubtreeFound, - dag_language_model_wave1, - parse_subtree_find_production_captured -} -import v2.std.collection { Absent, Optional, Present } -import v2.std.diagnostic { Accepted, Outcome, Rejected } -import v2.std.logic { Bool } -import v2.std.node { Node, Symbol } -import v2.std.text { String } - -data r1_surface_subject_note: String = "Catches a real quadratic end-to-end: real source -> census ingest (tokenize/parse/normalize) -> locate the fold call -> fold_call_to_r1_subject distills the surface fold body into R1's fold-step subject -> r1_judge_fold_step. The RED (list_append(left: acc, right: x)) has the accumulator in list_append's copied (left) port, so R1 projects Poly(2). The GREEN uses the SAME combiner with the accumulator flipped to the non-copied (right) port (list_append(left: x, right: acc)) — clean — isolating the copied-port check as the sole difference. The REFUSE control is an identity-body fold (fn(acc, x) { acc }) with no two-argument combiner call: the distiller refuses (fail-closed), never fabricating a subject that R1 would read as clean. COVERAGE BOUNDARY (real_branch_body_quadratic_is_currently_missed): challenged against the ACTUAL corpus suspect shape (src/v2/workflow/glob_discovery_law.dag: fold_list with the copying list_append(left: acc, right: Cons{..}) buried inside an if-branch and a struct-literal grow-by-one arg), the distiller MISSES it — verified by execution it refuses with cause port1_opaque because it reads the if-CONDITION (a one-argument call) as the combiner rather than looking inside the branch. That test is a RED that flips to FAIL the moment the distiller learns to traverse branches; the flip is the dissolution trigger to widen this marker into a positive catch. This is the honest signal that the mechanism, though green on the textbook shape, is not yet done on real code." - -data quadratic_snippet: String = "module quad\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) })\n}\n" - -data linear_snippet: String = "module lin\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { list_append(left: x, right: acc) })\n}\n" - -data identity_snippet: String = "module ident\n\nfn f(xs: List) -> Int {\n fold(xs, init: 0, f: fn(acc, x) { acc })\n}\n" - -data real_branch_body_snippet: String = "module rs\n\nfn g(xs: List) -> Int {\n fold_list(xs: xs, empty: Empty, cons: fn(acc, r) {\n if pred(r: r) {\n list_append(left: acc, right: Cons { head: r, tail: Empty })\n } else {\n acc\n }\n })\n}\n" - -fn ingest(source_text: String, file: Symbol) -> Optional { - let lm = dag_language_model_wave1() - match tokenize(text: source_text, file: file, rules: lm.lex) { - Rejected { diagnostics: _ } => Absent - Accepted { value: ts, diagnostics: _ } => - match parse_module(tokens: ts, grammar: lm.grammar) { - Rejected { diagnostics: _ } => Absent - Accepted { value: artifact, diagnostics: _ } => - match normalize(parse_tree: artifact.tree) { - Rejected { diagnostics: _ } => Absent - Accepted { value: tree, diagnostics: _ } => Present { value: tree } - } - } - } -} - -fn locate_fold_call(root: Node) -> Optional { - match parse_subtree_find_production_captured(root: root, emitted: ^dag_surface_primary_expr) { - ParseSubtreeFound { captured: call } => Present { value: call } - ParseSubtreeAbsent => Absent - } -} - -fn located_subject(source_text: String, file: Symbol) -> Optional> { - match ingest(source_text: source_text, file: file) { - Absent => Absent - Present { value: tree } => - match locate_fold_call(root: tree) { - Absent => Absent - Present { value: call } => Present { value: fold_call_to_r1_subject(fold_call: call) } - } - } -} - -test fn quadratic_fold_projects_poly_two() -> Bool { - match located_subject(source_text: quadratic_snippet, file: ^quad_file) { - Absent => false - Present { value: outcome } => - match outcome { - Rejected { diagnostics: _ } => false - Accepted { value: subject, diagnostics: _ } => - match r1_judge_fold_step(n: subject) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => true - R1Clean { flow_opaque_count: _ } => false - R1MalformedSubject => false - } - } - } -} - -test fn linear_fold_is_clean() -> Bool { - match located_subject(source_text: linear_snippet, file: ^lin_file) { - Absent => false - Present { value: outcome } => - match outcome { - Rejected { diagnostics: _ } => false - Accepted { value: subject, diagnostics: _ } => - match r1_judge_fold_step(n: subject) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => false - R1Clean { flow_opaque_count: _ } => true - R1MalformedSubject => false - } - } - } -} - -test fn identity_body_fold_refuses() -> Bool { - match located_subject(source_text: identity_snippet, file: ^ident_file) { - Absent => false - Present { value: outcome } => - match outcome { - Rejected { diagnostics: _ } => true - Accepted { value: _, diagnostics: _ } => false - } - } -} - -test fn real_branch_body_quadratic_is_currently_missed() -> Bool { - match located_subject(source_text: real_branch_body_snippet, file: ^rs_file) { - Absent => false - Present { value: outcome } => - match outcome { - Rejected { diagnostics: _ } => true - Accepted { value: subject, diagnostics: _ } => - match r1_judge_fold_step(n: subject) { - R1PolyTwoSuspect { implied_cost: _, flow_opaque_count: _ } => false - R1Clean { flow_opaque_count: _ } => true - R1MalformedSubject => true - } - } - } -} From 5250506ec86f90e015a713b6d69bdcdbfe530dcd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 9 Jul 2026 19:34:20 +0000 Subject: [PATCH 9/9] WIP: complexity --- src/v2/extdeps/languages/dag.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 849a32b7399..f788a146713 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -2302,7 +2302,7 @@ fn dag_grammar_expr_list_helper() -> GrammarExpr { } fn dag_grammar_untyped_params_helper() -> GrammarExpr { - dag_grammar_comma_list_expr(item: dag_grammar_terminal_lexeme(token_class: ^dag_token_ident)) + dag_grammar_comma_list_expr(item: dag_grammar_terminal(token_class: ^dag_token_ident)) } fn dag_grammar_postfix_call_suffix_expr() -> GrammarExpr { @@ -2362,7 +2362,7 @@ fn dag_grammar_primary_expr_expr() -> GrammarExpr { fn dag_grammar_primary_expr_core() -> GrammarExpr { dag_grammar_choice( left: dag_grammar_sequence( - left: dag_grammar_terminal_lexeme(token_class: ^dag_token_ident), + left: dag_grammar_terminal(token_class: ^dag_token_ident), right: dag_grammar_primary_ident_suffix_expr() ), right: dag_grammar_choice(