:Lens<EmissionProvenance> carrier + structural lens shape

src/v3/compiler/tests/integration.rs

@@ -57,6 +57,8 @@ mod cross_target_coverage_carrier_test;
 mod e6_g1a_option3_static_lens_test;
 #[path = "integration/e_i_lane_induction_preflight_test.rs"]
 mod e_i_lane_induction_preflight_test;
+#[path = "integration/emission_provenance_lens_test.rs"]
+mod emission_provenance_lens_test;
 #[path = "integration/extdeps_rust_primitives_loader_test.rs"]
 mod extdeps_rust_primitives_loader_test;
 #[path = "integration/four_fixture_regression_test.rs"]

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

@@ -0,0 +1,334 @@
+//! **Layer:** integration
+//!
+//! Cementing test for `Lens<List<EmissionProvenance>>` per Director Q1
+//! (a) RATIFIED at gunbc#1739 #issuecomment-4392562911 (per-Behavior
+//! Lens<C>-compatible framing). Brief:
+//! `docs/briefs/r3-substrate-emission-provenance-lens-worker.md`.
+//!
+//! **Scope of this slice — STRUCTURAL.** This test cements the
+//! substrate-shape contract: the `EmissionProvenance` record carrier and
+//! the lens fns/types compile, declare the Director-locked field set,
+//! and the lens binds against the correct carrier under a fixture-bound
+//! `data` declaration (matching the `mini_lens` precedent at
+//! `e6_g1a_option3_static_lens_test.rs:66-73`).
+//!
+//! **Behavioral round-trip is BEHAVIORALLY DEFERRED** — emitter writes
+//! field-path → lens recovers same field-path; per-Behavior list flatten
+//! matches per-line view. Producer wiring lives in
+//! `src/v3/compiler/src/emit/rust_target.rs`'s `render_named_template`
+//! call sites and is a separate downstream slice (precedent: `lenses.cost`
+//! BEHAVIORALLY PROXY).
+//!
+//! **Substrate-cascade receipt** — promoting the lens instance from a
+//! fixture-bound `data` declaration to a top-level `data` item in
+//! `src/v3/lenses/emission_provenance.dag` is currently blocked by
+//! Class 5 Gap 3 (top-level `ValueBody` boundary; sum-variant literals
+//! like `Empty` don't lower in `data` body context). Same constraint
+//! that blocks the canonical generic `data list_monoid<element>:
+//! Monoid<List<element>>` declaration documented at
+//! `src/v3/std/list.dag:61-64`. Dissolution trigger: when Class 5 Gap 3
+//! closes, this fixture promotes to a top-level `data` declaration in
+//! the lens .dag file without lens-shape changes.
+
+use std::collections::HashSet;
+
+use crate::common::cached_compile_to_dag;
+use v3_compiler::dag::TypeConnective;
+use v3_compiler::generated_full_bootstrap_dag;
+
+#[test]
+fn emission_provenance_record_has_locked_three_field_shape_with_locked_field_types() {
+    // Director-locked record shape per brief Deliverable 1
+    // (codex BLOCKING reshape at PR #1910 sha 2ed1046e Finding #1
+    // applied: record form, not coproduct; mandatory `rule` enforces
+    // structural fail-closed; optional `source_span` is structurally
+    // legal absence).
+    //
+    // Per openai-pro NON-BLOCKING TESTING finding (sha 6251a1e5): also
+    // assert each field's *type* (not just label) so the test fails if
+    // `rule` stops being `EmissionRule` or `source_span` stops being
+    // `OptionalSourceSpan`.
+    let dag = generated_full_bootstrap_dag();
+    let decl = dag
+        .declaration_by_name("EmissionProvenance")
+        .expect("EmissionProvenance missing from bootstrap");
+    let TypeConnective::Conj { children } = &decl.connective else {
+        panic!(
+            "EmissionProvenance is not a Conj record: {:?}",
+            decl.connective
+        );
+    };
+    let labels: Vec<&str> = children.iter().map(|f| f.label.as_str()).collect();
+    // Arity check first — `HashSet` collapses duplicates, so a record with
+    // (e.g.) `rule` declared twice would pass the set comparison below.
+    // Assert exact arity to catch duplicate / extra fields explicitly.
+    assert_eq!(
+        children.len(),
+        3,
+        "EmissionProvenance must declare exactly 3 fields (emitted_line, rule, \
+         source_span); actual labels: {labels:?}"
+    );
+    let expected_labels: HashSet<&str> = ["emitted_line", "rule", "source_span"]
+        .into_iter()
+        .collect();
+    let actual_labels: HashSet<&str> = labels.iter().copied().collect();
+    assert_eq!(
+        actual_labels, expected_labels,
+        "EmissionProvenance must carry the Director-locked 3-field record shape; \
+         actual labels: {labels:?}"
+    );
+
+    // Each field's type must resolve to the locked carrier — not a
+    // structural look-alike. If the carrier downstream weakens (e.g.,
+    // `rule: String` instead of `rule: EmissionRule`), this fails.
+    let emission_rule = dag
+        .declaration_by_name("EmissionRule")
+        .expect("EmissionRule missing from bootstrap");
+    let optional_source_span = dag
+        .declaration_by_name("OptionalSourceSpan")
+        .expect("OptionalSourceSpan missing from bootstrap");
+    let positive_int = dag
+        .declaration_by_name("PositiveInt")
+        .expect("PositiveInt missing from bootstrap");
+
+    for field in children {
+        match field.label.as_str() {
+            "emitted_line" => assert_eq!(
+                field.ty, positive_int.id,
+                "EmissionProvenance.emitted_line must resolve to `PositiveInt`"
+            ),
+            "rule" => assert_eq!(
+                field.ty, emission_rule.id,
+                "EmissionProvenance.rule must resolve to `EmissionRule`"
+            ),
+            "source_span" => assert_eq!(
+                field.ty, optional_source_span.id,
+                "EmissionProvenance.source_span must resolve to `OptionalSourceSpan`"
+            ),
+            other => panic!("unexpected EmissionProvenance field: {other}"),
+        }
+    }
+}
+
+// Note: the standalone `emitted_line_is_positive_int_refinement_not_bare_int`
+// test (codex BLOCKING finding sha 6c7c3d85) is now subsumed by
+// `emission_provenance_record_has_locked_three_field_shape_with_locked_field_types`
+// above, which asserts each field's type explicitly (including
+// `emitted_line: PositiveInt`).
+
+#[test]
+fn production_lens_module_compiles_cleanly() {
+    // Per openai-pro NON-BLOCKING TESTING finding (sha 4553d4e8): the
+    // fixture-bound `#[ignore]`d test below mirrors the production lens
+    // file but doesn't actively guard it — `src/v3/lenses/emission_provenance.dag`
+    // could drift syntactically or type-wise without any active test
+    // failing. This smoke compiles the production .dag file directly
+    // (it lives outside the bootstrap, like other `src/v3/lenses/*.dag`
+    // entries — compare `lens_apply.rs:1020` for `named_function_count.dag`),
+    // so syntactic / type drift fails this test instead of slipping
+    // through.
+    let _dag = cached_compile_to_dag(
+        include_str!("../../../lenses/emission_provenance.dag"),
+        "src/v3/lenses/emission_provenance.dag",
+    );
+}
+
+#[test]
+fn optional_source_span_carries_none_and_some_arms_with_locked_payload() {
+    // v3 std has no generic Option<T>; the typed-sum pattern is the
+    // idiom (compare `OptionalDiagnostic` at `v3.std.dimensions`).
+    // NoSourceSpan must be a structurally legal absence (NOT a
+    // diagnostic) per Director `feedback_no_textual_enforcement_bridges`.
+    //
+    // Per openai-pro NON-BLOCKING TESTING finding (sha 6251a1e5):
+    // assert that the `SomeSourceSpan` variant payload resolves to the
+    // canonical `SourceSpan` carrier so the test fails if the payload
+    // gets weakened or renamed.
+    let dag = generated_full_bootstrap_dag();
+    let decl = dag
+        .declaration_by_name("OptionalSourceSpan")
+        .expect("OptionalSourceSpan missing from bootstrap");
+    let TypeConnective::Disj { variants } = &decl.connective else {
+        panic!(
+            "OptionalSourceSpan is not a Disj sum: {:?}",
+            decl.connective
+        );
+    };
+    // Arity first — `HashSet` collapses duplicates; assert exact variant
+    // count to catch a duplicate `SomeSourceSpan` declaration etc.
+    assert_eq!(
+        variants.len(),
+        2,
+        "OptionalSourceSpan must declare exactly 2 variants (NoSourceSpan, \
+         SomeSourceSpan); actual variants: {:?}",
+        variants.iter().map(|v| &v.label).collect::<Vec<_>>()
+    );
+    let actual_labels: HashSet<&str> = variants.iter().map(|v| v.label.as_str()).collect();
+    let expected_labels: HashSet<&str> = ["NoSourceSpan", "SomeSourceSpan"].into_iter().collect();
+    assert_eq!(
+        actual_labels, expected_labels,
+        "OptionalSourceSpan must be the 2-variant typed-sum shape \
+         (NoSourceSpan structurally legal; SomeSourceSpan {{ value: SourceSpan }})"
+    );
+
+    // The `SomeSourceSpan` variant's payload type must resolve to the
+    // canonical `SourceSpan` from `dsl/std/types.dag` (re-exported via
+    // `v3.std.substrate`), not a structural look-alike. The
+    // `value` field on the variant payload is what carries the
+    // SourceSpan reference.
+    let some_variant = variants
+        .iter()
+        .find(|v| v.label == "SomeSourceSpan")
+        .expect("SomeSourceSpan variant missing");
+    let some_payload = dag.declaration(some_variant.ty);
+    let TypeConnective::Conj {
+        children: some_children,
+    } = &some_payload.connective
+    else {
+        panic!(
+            "SomeSourceSpan variant payload should be a record with a single `value: SourceSpan` \
+             field; actual payload connective: {:?}",
+            some_payload.connective
+        );
+    };
+    // Assert exact arity — `find()` would let `SomeSourceSpan { value, extra }`
+    // pass even though the locked shape names a single payload field.
+    assert_eq!(
+        some_children.len(),
+        1,
+        "SomeSourceSpan must declare exactly 1 payload field (`value: SourceSpan`); \
+         actual fields: {:?}",
+        some_children.iter().map(|f| &f.label).collect::<Vec<_>>()
+    );
+    let value_field = some_children
+        .iter()
+        .find(|f| f.label == "value")
+        .expect("SomeSourceSpan payload missing `value` field");
+    let source_span = dag
+        .declaration_by_name("SourceSpan")
+        .expect("SourceSpan missing from bootstrap");
+    assert_eq!(
+        value_field.ty, source_span.id,
+        "SomeSourceSpan.value must resolve to `SourceSpan`, not a structural look-alike"
+    );
+
+    // NoSourceSpan must be a unit variant (no payload fields). A drift
+    // to e.g. `NoSourceSpan { value: SourceSpan }` would silently make
+    // it indistinguishable from `SomeSourceSpan` — assert empty payload.
+    let none_variant = variants
+        .iter()
+        .find(|v| v.label == "NoSourceSpan")
+        .expect("NoSourceSpan variant missing");
+    let none_payload = dag.declaration(none_variant.ty);
+    if let TypeConnective::Conj {
+        children: none_children,
+    } = &none_payload.connective
+    {
+        assert_eq!(
+            none_children.len(),
+            0,
+            "NoSourceSpan must be a unit variant (no payload fields) — \
+             a payload-bearing NoSourceSpan would collapse the absence/presence \
+             distinction with SomeSourceSpan; actual fields: {:?}",
+            none_children.iter().map(|f| &f.label).collect::<Vec<_>>()
+        );
+    }
+    // Other connective kinds (e.g., the unit/Top connective the lowerer
+    // synthesizes for unit variants) are also acceptable; the only
+    // fail-condition is a payload-bearing NoSourceSpan.
+}
+
+// Fixture-bound lens instance per the `mini_lens` precedent at
+// `e6_g1a_option3_static_lens_test.rs:66-73`. The string source declares
+// the carrier inline + the lens fns + the `data emission_provenance_lens:
+// Lens<List<EmissionProvenance>>` instance. This is the cementing form
+// for the Director-locked 6-field `Lens<C>` shape against the
+// `List<EmissionProvenance>` carrier; promotion to a top-level `data`
+// item in `src/v3/lenses/emission_provenance.dag` blocks on Class 5
+// Gap 3 closure (sum-variant `Empty` literal in data body context).
+const LENS_FIXTURE_SOURCE: &str = r#"
+import std.integer { PositiveInt }
+import std.list { List, Empty, concat }
+import std.substrate { Dag, Behavior, LoopBound }
+import v3.std.dimensions { Witness, OptionalDiagnostic }
+import v3.std.diagnostics { Diagnostic }
+import v3.std.lens { Lens }
+import v3.std.substrate { SourceSpan }
+
+type EmissionRule = String
+
+type OptionalSourceSpan
+  = NoSourceSpan
+  | SomeSourceSpan { value: SourceSpan }
+
+type EmissionProvenance {
+  emitted_line: PositiveInt
+  rule: EmissionRule
+  source_span: OptionalSourceSpan
+}
+
+// Lowering seeds for `List<EmissionProvenance>.Empty` — same shape as
+// the `_e6_seed_list_*_empty` pattern at e6_g1a_option3_static_lens_test.rs:45-48.
+fn _seed_list_provenance_empty() -> List<EmissionProvenance> = Empty
+
+fn read_provenance(d: Dag, b: Behavior) -> Witness<List<EmissionProvenance>> =
+  Inhabits(_seed_list_provenance_empty())
+
+fn empty_provenance_list() -> List<EmissionProvenance> = Empty
+
+fn concat_provenance(
+  a: List<EmissionProvenance>,
+  b: List<EmissionProvenance>
+) -> List<EmissionProvenance> = concat(a, b)
+
+fn branch_provenance(
+  l: List<EmissionProvenance>,
+  r: List<EmissionProvenance>
+) -> List<EmissionProvenance> = concat(l, r)
+
+fn iterate_provenance(
+  c: List<EmissionProvenance>,
+  bound: LoopBound
+) -> List<EmissionProvenance> = c
+
+fn validate_provenance(d: Dag, c: List<EmissionProvenance>) -> OptionalDiagnostic =
+  NoDiagnostic
+
+data emission_provenance_lens: Lens<List<EmissionProvenance>> = {
+  name: "EmissionProvenance",
+  read: read_provenance,
+  sequential: { op: concat_provenance, identity: empty_provenance_list },
+  branch: branch_provenance,
+  iterate: iterate_provenance,
+  validate: validate_provenance
+}
+"#;
+
+#[test]
+#[ignore = "blocked on Class 5 Gap 3 (top-level ValueBody boundary at \
+            src/v3/compiler/src/dag.rs:259-287): `data emission_provenance_lens: \
+            Lens<List<EmissionProvenance>>` rejects on two facets of the same \
+            gap — bare sum-variant identity (`identity: Empty`) doesn't lower \
+            in data body context, AND nested-fn identity (`identity: \
+            empty_provenance_list`) hits the opaque-body rejection for \
+            fn-typed fields in data bodies. Same constraint blocks the \
+            canonical `data list_monoid<element>: Monoid<List<element>>` at \
+            `src/v3/std/list.dag:61-64`. Dissolution trigger: when both facets \
+            close (top-level List/sum-variant ValueBody carriers AND fn-typed \
+            data-body fields validate structurally), un-ignore and verify this \
+            test passes without lens-shape changes. See lens .dag file header \
+            for the unified two-facet receipt."]
+fn emission_provenance_lens_binds_against_locked_carrier() {
+    // Structural cement: the `Lens<List<EmissionProvenance>>` instance
+    // compiles against the Director-locked 6-field `Lens<C>` carrier at
+    // `src/v3/std/lens.dag` under the fixture-bound pattern.
+    //
+    // Currently `#[ignore]`d on the substrate-cascade STOP described in
+    // the test attribute. The fixture source IS authored in
+    // `LENS_FIXTURE_SOURCE` so the dissolution trigger is the simple
+    // act of removing this `#[ignore]` once Class 5 Gap 3 closes.
+    let _dag = cached_compile_to_dag(
+        LENS_FIXTURE_SOURCE,
+        "tests/integration/emission_provenance_lens_test.rs:LENS_FIXTURE_SOURCE",
+    );
+}

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

@@ -31,7 +31,7 @@ src/v3/std/anthropic_operations.dag	6	3404	a729e7662be9af5f
 src/v3/std/anthropic_schema.dag	12	54190	a430f932e3962ecb
 src/v3/std/approximate_field.dag	11	16864	fb342d17eec1c8ac
 src/v3/std/bin_shim.dag	4	2544	9ac96f1b3feafe47
-src/v3/std/bootstrap_authority.dag	4	66427	908aa66838dfb9e6
+src/v3/std/bootstrap_authority.dag	4	67475	1d59dad2bb459e05
 src/v3/std/bridge_ledger.dag	7	31662	ec3b4ea8c0455eb7
 src/v3/std/clean_emission.dag	15	23867	e7bc1e6145f4781e
 src/v3/std/computation.dag	18	36754	8023f388c3fb0918
@@ -40,6 +40,7 @@ src/v3/std/cross_target_coverage.dag	10	373515	814a9a617f609ad3
 src/v3/std/diagnostics.dag	11	21478	7d2e9e73d74e5adb
 src/v3/std/dimensions.dag	21	39170	c6833b618a39e0af
 src/v3/std/effects.dag	53	97984	1acdbeaa68acfd2e
+src/v3/std/emission_provenance.dag	6	4966	ac93c5c74cb4f9f9
 src/v3/std/emit_model.dag	44	83040	71640f0720ab903a
 src/v3/std/extdeps_bootstrap_fixtures.dag	4	16839	22cffc76152e82dd
 src/v3/std/go_method_template_contracts.dag	14	133273	43ccd439b5e388ea

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

@@ -349,6 +349,13 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[
     // receipts per #1857). SG-0 ratchet: new hand-authored integration test.
     "src/v3/compiler/tests/integration/e6_g1a_option3_static_lens_test.rs",
     "src/v3/compiler/tests/integration/e_i_lane_induction_preflight_test.rs",
+    // T-Substrate-Lens-Primitive Lens<EmissionProvenance> structural cementing
+    // test (PR #1928). Per Director Q1(a) RATIFIED at gunbc#1739
+    // #issuecomment-4392562911. Hand-authored entry added per SG-0 census
+    // discipline; integration-test home (matches `mini_lens` /
+    // `e6_g1a_option3_static_lens_test` precedent for fixture-bound lens
+    // instances).
+    "src/v3/compiler/tests/integration/emission_provenance_lens_test.rs",
     // T-Ground-Engine Phase-1 loader-close (PR #776, Director-approved
     // Path 2): hand-Rust integration test pinning
     // `Dag::rust_pilot_primitives()` type-structure walk + the