T-Lens API

docs/v3-lens-capability-register.md

@@ -47,6 +47,7 @@ A lens is only "done" when **both** axes are at their strongest grade for the sc
 | `structural_resolution.dag` | TERMINAL | COMPLETE | None (v3-native) | `List<UnresolvedArrowBody>` (regression pin) | N/A |
 | `infer_helpers.dag` | PARTIAL | N/A | None | Bounded Cat-1/Cat-2 infer helpers only | N/A (see file header for scope — `predicate_info`, `walk_to_optional_cardinality_decl`, `callable_template_arguments`, `is_retryable_generic_decl_walk`, `declaration_is_callable`, `template_arguments_match` stay in Rust pending substrate work) |
 | `lower_helpers.dag` | PARTIAL | N/A | None | `expr_span(expr) -> SourceSpan` only | N/A (see file header — `SurfaceLiteral -> LiteralBits` and tuple-variant helper rejected on emit gaps; wire-in parked on parse/parse_surface convergence) |
+| `named_function_count.dag` | TERMINAL | **N/A** | None (demo / Day-1 gate fixture) | `Int` (count of `Bind` nodes with non-empty `name`) | N/A (not in `Dag::new()` bootstrap; `compile_to_dag` integration receipt — not `regen.dag`) |
 
 ## Common root causes
 

src/v3/compiler/build.rs

@@ -2,14 +2,13 @@
 // directories and generate Rust arrays of `(path, content)` pairs
 // the bootstrap loader consumes.
 //
-// Three generated arrays exist:
-//   - `STAGED_FILES`   for `src/v3/std/*.dag`
-//   - `V3_SPECS`       for `src/v3/spec/*.dag`
-//   - `COMPILER_FILES` for `src/v3/compiler/*.dag` (except `tokenize.dag`; see below)
+// Generated arrays:
+//   - `STAGED_FILES`          for `src/v3/std/*.dag`
+//   - `V3_SPECS`              for `src/v3/spec/*.dag`
+//   - `COMPILER_FILES`        for `src/v3/compiler/*.dag` (except `tokenize.dag`; see below)
 //
-// Adding a new staged std/spec/compiler file becomes a pure file-system
-// change — no Rust edits to `bootstrap.rs`, no fixture-array
-// maintenance, no skip-list drift.
+// Adding a new staged std/spec/compiler file becomes a pure file-system change
+// — no Rust edits to `bootstrap.rs`, no fixture-array maintenance, no skip-list drift.
 //
 // **Why a build script.** The pre-unwind shape used hardcoded
 // `const RUST_DAG: &str = include_str!("../../spec/rust.dag");`
@@ -256,7 +255,6 @@ fn main() {
         &gunbc_dir,
         &gunbc_entries,
     );
-
     let out_dir = env::var("OUT_DIR").expect("OUT_DIR must be set by Cargo");
     let out_dir = Path::new(&out_dir);
     let staged_out = out_dir.join("v3_staged_files.rs");

src/v3/compiler/tests/fixtures/r1_gates.dag

@@ -0,0 +1,23 @@
+// std.r1_gates - Day-1 R1 gate declarations (integration-test fixture).
+//
+// `TestClaim.source` is the full user lens program text (same bytes as
+// `src/v3/lenses/named_function_count.dag`); `m1_5_user_authored_lens_gate_test`
+// asserts lockstep so the claim stays single-authority for the compile receipt.
+// Integration test then `compile_to_dag`s that extracted `source` (runner-shaped
+// `Compiles` receipt). Payload is a standalone `module lenses.named_function_count`
+// unit (imports std only), not a consumer that imports this module from bootstrap.
+//
+// Lives under `src/v3/compiler/tests/fixtures/` so it is **not** auto-staged
+// into `Dag::new()` bootstrap (`src/v3/std/*.dag` is build-script enumerated).
+
+module std.r1_gates
+
+import std.verification { TestClaim }
+
+data user_authored_lens_compiles_gate: TestClaim = {
+  name: "user_authored_lens_compiles",
+  source: "// lenses.named_function_count - minimal user-authored lens (Day-1 gate demo).\n//\n// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY N/A.\n// See docs/v3-lens-capability-register.md.\n//\n// **Not** bundled into `Dag::new()` bootstrap: it compiles externally via\n// `compile_to_dag` (see `m1_5_user_authored_lens_gate_test`). Demo only:\n// counts `Bind` behaviors whose `name` is non-empty. Not in `regen.dag`.\n\nmodule lenses.named_function_count\n\nimport std.list { fold }\nimport std.substrate { Dag, Behavior }\n\nfn count_named_bind(behavior: Behavior) -> Int =\n  match behavior {\n    Value(v) => 0\n    Transform(t) => 0\n    Branch(b) => 0\n    Loop(l) => 0\n    Bind(bind) => if bind.name == \"\" then 0 else 1\n  }\n\nfn named_function_count(d: Dag) -> Int =\n  fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior))\n",
+  file_name: "src/v3/lenses/named_function_count.dag",
+  predicate: Compiles,
+  requires: []
+}

src/v3/compiler/tests/integration.rs

@@ -73,6 +73,8 @@ mod m1_4_emit_python_test;
 mod m1_5_emit_omni_demo_test;
 #[path = "integration/m1_5_testgen_test.rs"]
 mod m1_5_testgen_test;
+#[path = "integration/m1_5_user_authored_lens_gate_test.rs"]
+mod m1_5_user_authored_lens_gate_test;
 #[path = "integration/m1_5_verification_test.rs"]
 mod m1_5_verification_test;
 #[path = "integration/m1_fn_external_body_reconciliation_test.rs"]

src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs

@@ -0,0 +1,105 @@
+//! **Layer:** integration
+//!
+//! Day-1 R1 gate `user_authored_lens_compiles`: the gate fixture carries a
+//! `TestClaim` whose `source` / `file_name` are the single authority for what a
+//! future runner would compile; this module asserts lockstep with the on-disk
+//! lens file, then compiles that payload via `compile_to_dag` on top of the
+//! standard bootstrap context (`Dag::new()`), without bundling the lens into the
+//! bootstrap.
+//!
+//! **Behavior receipt (TESTING.md):** `user_authored_lens_testclaim_payload_tracks_on_disk_lens_and_compiles`
+//! lowers the gate fixture, reads `source` off the lowered `TestClaim`, and runs
+//! `compile_to_dag` on that string — this is the executable `Compiles` path, not
+//! merely “the record literal typechecks.” The payload is the **entire**
+//! `lenses.named_function_count` module text (same bytes as the `.dag` file); it
+//! intentionally does **not** use `import lenses.named_function_count { ... }`
+//! from a second file, because that pattern would require the lens to live in
+//! `Dag::new()` bootstrap, which this demo deliberately avoids.
+
+use v3_compiler::compile_to_dag;
+use v3_compiler::dag::{Dag, FieldValue, LiteralBits, ValueBody};
+use v3_compiler::CompileError;
+
+const R1_GATES_SOURCE: &str = include_str!("../fixtures/r1_gates.dag");
+const ON_DISK_LENS: &str = include_str!("../../../lenses/named_function_count.dag");
+
+fn testclaim_string_field(dag: &Dag, gate_name: &str, label: &str) -> String {
+    let decl = dag
+        .declaration_by_name(gate_name)
+        .unwrap_or_else(|| panic!("missing declaration `{gate_name}`"));
+    let Some(ValueBody::Structural { fields }) = &decl.value_body else {
+        panic!("`{gate_name}` should carry a structural value body");
+    };
+    fields
+        .iter()
+        .find(|(l, _)| l == label)
+        .and_then(|(_, v)| match v {
+            FieldValue::Literal(LiteralBits::String(s)) => Some(s.clone()),
+            _ => None,
+        })
+        .unwrap_or_else(|| panic!("`{gate_name}` missing String field `{label}`"))
+}
+
+fn assert_compile_clean(source: &str, file_name: &str, label: &str) {
+    match compile_to_dag(source, file_name) {
+        Ok(dag) => assert!(
+            dag.diagnostics().is_empty(),
+            "{label} should compile with no diagnostics, got {:?}",
+            dag.diagnostics().iter().collect::<Vec<_>>()
+        ),
+        Err(CompileError::Semantic(d)) => panic!(
+            "{label} compile failed: {:?}",
+            d.diagnostics().iter().collect::<Vec<_>>()
+        ),
+        Err(other) => panic!("{label}: unexpected compile error: {other:?}"),
+    }
+}
+
+#[test]
+fn r1_gates_fixture_compiles_against_bootstrap_context() {
+    assert_compile_clean(
+        R1_GATES_SOURCE,
+        "src/v3/compiler/tests/fixtures/r1_gates.dag",
+        "gate fixture `r1_gates.dag`",
+    );
+}
+
+#[test]
+fn user_authored_lens_testclaim_payload_tracks_on_disk_lens_and_compiles() {
+    let gate_dag = match compile_to_dag(
+        R1_GATES_SOURCE,
+        "src/v3/compiler/tests/fixtures/r1_gates.dag",
+    ) {
+        Ok(dag) => dag,
+        Err(CompileError::Semantic(d)) => panic!(
+            "gate fixture compile failed: {:?}",
+            d.diagnostics().iter().collect::<Vec<_>>()
+        ),
+        Err(other) => panic!("gate fixture: unexpected compile error: {other:?}"),
+    };
+    assert!(
+        gate_dag.diagnostics().is_empty(),
+        "gate fixture should load cleanly, got {:?}",
+        gate_dag.diagnostics().iter().collect::<Vec<_>>()
+    );
+
+    let source = testclaim_string_field(&gate_dag, "user_authored_lens_compiles_gate", "source");
+    let file_name =
+        testclaim_string_field(&gate_dag, "user_authored_lens_compiles_gate", "file_name");
+
+    assert_eq!(
+        source, ON_DISK_LENS,
+        "`TestClaim.source` must stay byte-identical to `src/v3/lenses/named_function_count.dag` \
+         (single authority for the user lens program; update both together)"
+    );
+    assert_eq!(
+        file_name, "src/v3/lenses/named_function_count.dag",
+        "`TestClaim.file_name` should name the on-disk lens path for the Day-1 witness"
+    );
+
+    assert_compile_clean(
+        &source,
+        &file_name,
+        "TestClaim `source` payload (read from gate fixture)",
+    );
+}

src/v3/compiler/tests/integration/parse_corpus_manifest.txt

@@ -17,9 +17,9 @@ src/v3/compiler/tests/four_fixture_pressure/id.v3	2	2452	ec8b40edc3d3c017
 src/v3/compiler/tests/four_fixture_pressure/is_empty.v3	3	6755	00117f14eb43dd20
 src/v3/compiler/tests/four_fixture_pressure/wrap.v3	4	5189	ac633b042c944480
 src/v3/compiler/tokenize.dag	27	56809	37569b3f9fb2e6fa
-src/v3/spec/go.dag	118	1052995	e4cbb0018a029584
-src/v3/spec/python.dag	86	550491	a66ba9ecf2f22c95
-src/v3/spec/rust.dag	132	1115113	6a9b8a3ba230bb7b
+src/v3/spec/go.dag	118	1052999	a606d7ea68a22076
+src/v3/spec/python.dag	86	550494	b896e4c15bd6addc
+src/v3/spec/rust.dag	132	1115115	1110c001009a9065
 src/v3/spec/v3_l1.dag	8	2238	1f55d782265c3bfe
 src/v3/std/algebra.dag	33	281947	fd777e369473acfb
 src/v3/std/clean_emission.dag	15	23867	e7bc1e6145f4781e

src/v3/compiler/tests/integration/sg0_census_test.rs

@@ -211,6 +211,7 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
     "src/v3/compiler/tests/integration/m1_3_lens_cost_test.rs",
     "src/v3/compiler/tests/integration/m1_3_lens_unused_parameters_test.rs",
     "src/v3/compiler/tests/integration/m1_5_testgen_test.rs",
+    "src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs",
     "src/v3/compiler/tests/integration/m1_5_verification_test.rs",
     "src/v3/compiler/tests/integration/m1_fn_external_body_reconciliation_test.rs",
     "src/v3/compiler/tests/integration/m1_lens_structural_resolution_test.rs",

src/v3/lenses/named_function_count.dag

@@ -0,0 +1,25 @@
+// lenses.named_function_count - minimal user-authored lens (Day-1 gate demo).
+//
+// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY N/A.
+// See docs/v3-lens-capability-register.md.
+//
+// **Not** bundled into `Dag::new()` bootstrap: it compiles externally via
+// `compile_to_dag` (see `m1_5_user_authored_lens_gate_test`). Demo only:
+// counts `Bind` behaviors whose `name` is non-empty. Not in `regen.dag`.
+
+module lenses.named_function_count
+
+import std.list { fold }
+import std.substrate { Dag, Behavior }
+
+fn count_named_bind(behavior: Behavior) -> Int =
+  match behavior {
+    Value(v) => 0
+    Transform(t) => 0
+    Branch(b) => 0
+    Loop(l) => 0
+    Bind(bind) => if bind.name == "" then 0 else 1
+  }
+
+fn named_function_count(d: Dag) -> Int =
+  fold(d.nodes, 0, |acc, behavior| acc + count_named_bind(behavior))

src/v3/spec/go.dag

@@ -42,7 +42,12 @@ data go_execution_model: TargetExecutionModel = {
 }
 
 data go_source_filtering: SourceFiltering = {
-  excluded_prefixes: ["dsl/std/", "src/v3/std/", "src/v3/spec/", "src/v3/compiler/"]
+  excluded_prefixes: [
+    "dsl/std/",
+    "src/v3/std/",
+    "src/v3/spec/",
+    "src/v3/compiler/",
+  ]
 }
 
 data go_execution_requirement: ExecutionModelRequirement = GarbageCollected

src/v3/spec/python.dag

@@ -144,7 +144,11 @@ data python_target: TargetExecutionModel = {
 }
 
 data python_source_filtering: SourceFiltering = {
-  excluded_prefixes: ["dsl/std/", "src/v3/std/", "src/v3/spec/"]
+  excluded_prefixes: [
+    "dsl/std/",
+    "src/v3/std/",
+    "src/v3/spec/",
+  ]
 }
 
 data python_execution_requirement: ExecutionModelRequirement = GarbageCollected

src/v3/spec/rust.dag

@@ -91,7 +91,12 @@ data rust_execution_model: TargetExecutionModel = {
 }
 
 data rust_source_filtering: SourceFiltering = {
-  excluded_prefixes: ["dsl/std/", "src/v3/std/", "src/v3/spec/", "src/v3/compiler/"]
+  excluded_prefixes: [
+    "dsl/std/",
+    "src/v3/std/",
+    "src/v3/spec/",
+    "src/v3/compiler/",
+  ]
 }
 
 data rust_execution_requirement: ExecutionModelRequirement = OwnershipBased