γ

docs/design-test-infra.md

@@ -195,10 +195,16 @@ The "more efficient than typical" intuition cashes out from ALL THREE collapses,
 
 1. **Exact syntax for `requires: List<ResourceReference>` on `TestClaim`.** Structural: should ResourceReference be a typed declaration reference (`DeclarationRef`) or a typed resource type (`ResourceHandle` in resources.dag terminology)? Probably the former — handles are runtime artifacts, not compile-time declarations. Verify at implementation time.
 
+   **Answered (R2.1, DB-15 impl PR):** ResourceReference is a typed compile-time declaration sentinel — "the former." Authored in `src/v3/std/verification.dag` as a 🟡 scaffold record `type ResourceReference { identifier: String }` pending the `dsl/std/resources.dag` → v3 port. The `identifier: String` carrier is bootstrap-local; post-port, the shape narrows to a `DeclarationRef` mirror that structurally rejects any non-`resource` declaration. `ResourceHandle` (runtime-minted opaque proof of acquisition) is explicitly NOT the referent type — handles are produced by the compiler's acquire nodes at runtime, which is the wrong layer for a compile-time test declaration. Kept distinct from the generic `DeclarationRef` sentinel so the narrowed accept set dissolves into the type itself once the `resource` keyword lands in v3.
+
 2. **Which existing `TestPredicate` variants need the `requires` declaration, and which are self-contained?** `PortStateExpectation` and `CostBounded` are compile-time assertions with no runtime resource needs. `BehavioralObservation` needs a test-runner resource. `MockBackedInvariant` needs both a test-runner AND a mock-transport resource. Open: is `requires` per-claim or per-predicate-variant?
 
+   **Answered (R2.1, DB-15 impl PR):** `requires` is per-claim. A single subject-under-test exercised by multiple predicate variants (compile check + behavioral observation + cost check) shares one resource declaration set because those needs are properties of the claim's execution context, not the predicate shape. Per-predicate-variant `requires` would duplicate the data across arms and admit an illegal-state combination where variants disagree about the required resources for the same subject. Compile-time predicates (`Compiles`, `FailsWithDiagnostic`, `PortHasState`, `CostBounded`) carry a single-element `requires: [{ identifier: "compile_time" }]`; runtime-backed predicates (`BehavioralObservation`, `MockBackedInvariant`) carry non-empty lists naming the test-runner plus any mock transports. The empty-list case is deferred to the post-resources-port window when v3 user-code empty-list-literal template inference also stabilizes.
+
 3. **Tautology-avoidance enforcement.** The rule "predicate cannot rerun the producing lens" is currently prose. Can it be enforced structurally — e.g., the predicate variants are explicitly behavioral/observational by type, and "rerun lens X" is not even expressible? Needs a pass to confirm no variant sneaks in that permits the pattern.
 
+   **Answered (R2.1, DB-15 impl PR):** Structurally enforced by the `TestPredicate` coproduct. No variant takes the lens's own output as its verification oracle. `BehavioralObservation` takes a `(subject, input_sample, expected_output)` triple where `expected_output` is a separately-declared `DeclarationRef` — the oracle is an independent declared value, not a lens rerun. `MockBackedInvariant` takes a `(subject, mock_transport, invariant)` triple where `invariant` is a separately-declared `DeclarationRef` asserting a property under the mocked observation. A hypothetical `LensSays { lens, subject, expected }` variant is NOT in the coproduct, and — per the `TestPredicate` docblock added in the impl PR — cannot be added without re-opening tautology avoidance in DB-15. `src/v3/compiler/tests/lane2_stage_2c_verification_smoke.rs::test_predicate_coproduct_blocks_lens_rerun_tautology` is the structural regression guard: it enumerates a set of forbidden variant names (`LensSays`, `LensEquals`, `LensOutput`, `RunLens`) and asserts none are in the coproduct. Lens outputs can still supply the *value* that seeds an `expected_output` or a `bound` (pre-computed at declaration time); the test runner does not rerun the lens at claim-check time.
+
 4. **Lane 2 Stage 2c generation surface.** Stage 2c generates `TestClaim` declarations from lens outputs. What's the structural shape of "this lens's output, materialized into a `TestPredicate`"? Likely one generation rule per `(lens, predicate-variant)` pair, declared once per lens. Out of scope for DB-15's design; in scope for Stage 2c's implementation.
 
 ---

src/v3/ROADMAP.md

@@ -513,11 +513,13 @@ Follow-up (not blocking): emission for narrowed ports currently errors if `emit_
 
 ### Lane 2 Stage 2c — test infrastructure
 
-**Deferral: DB-15 tests-as-declarations extensions (M, blocks Lane 2 Stage 2c).** Design doc (R2 draft): [design-test-infra.md](../../docs/design-test-infra.md). R2 consumes the compiler-as-dependency-analyzer thesis: tests are declarations (extending the existing `src/v3/std/verification.dag` `TestClaim`/`TestSuite` authority), resources are references to `dsl/std/resources.dag`, sharing/caching/incremental execution fall out of the compiler's existing dependency walk. No new caches or runner mechanisms — DB-15 names HOW things depend, then the walk does the rest.
+**Cleared (this PR, DB-15 R2 impl):** `src/v3/std/verification.dag` now carries the R2 extensions: `TestClaim.requires: List<ResourceReference>`, the two new runtime-backed `TestPredicate` variants (`BehavioralObservation { subject, input_sample, expected_output }` and `MockBackedInvariant { subject, mock_transport, invariant }`), and `fn materialize_obligations(suite: TestSuite) -> List<TestClaim>` as the dependency-walk entry point. R2's three open questions resolved in-PR: (1) `ResourceReference` is a typed compile-time declaration sentinel (scaffold shape `{ identifier: String }` pending resources-in-v3 port, narrows to `resource`-only `DeclarationRef` post-port — not a runtime `ResourceHandle`); (2) `requires` is per-claim, not per-predicate-variant; (3) tautology avoidance is structurally enforced by the coproduct shape. `dsl/gunbc/compiler.dag`-level Stage 2c acceptance smoke at `src/v3/compiler/tests/lane2_stage_2c_verification_smoke.rs` locks each of the three answers + the materialization entry point + a user-authored suite round-trip. Design: [design-test-infra.md](../../docs/design-test-infra.md) R2.
 
-Implementation scope (M, once design locks): extend `TestClaim` with `requires: List<ResourceReference>` and two new `TestPredicate` variants (`BehavioralObservation`, `MockBackedInvariant`); apply tautology-avoidance rule structurally; one-file migration proof. Yellow-flag threshold: design must lock before Lane 2 Stage 2c kickoff.
+**Remaining for Stage 2c kickoff (consumer side, separate PR):** a runner that reads `materialize_obligations(suite)` output, acquires each claim's `requires` resources, and executes the predicate. Out of scope for DB-15 per the R2 brief's consumer-contract deferral.
 
-**Prerequisite deferral: `dsl/std/resources.dag` → v3 reconciliation (S).** Zero references to `Resource`/`acquire`/`release` under `src/v3/` today. DB-15's `requires: List<ResourceReference>` is authored but unconsumed until this lands. Options: port declaration into `src/v3/std/resources.dag`, OR make `dsl/std/resources.dag` bootstrap-consumable by v3. Preferring the latter for single-authority. Separable from DB-15 implementation — can land independently. This is also a dissolution-of-dual-representation item; consider parking it in §Scheduled deletions if dsl/v3 duplication is the framing, or keep as a prerequisite deferral here. Preferring here for now since it's narrowly scoped.
+**Prerequisite deferral: `dsl/std/resources.dag` → v3 reconciliation (S).** Zero references to `Resource`/`acquire`/`release` under `src/v3/` today. `ResourceReference` is authored with a 🟡 scaffold marker carrying an `identifier: String` — when the port lands, it dissolves into a `DeclarationRef`-shape accepting only `resource` declarations (narrowing the accept set and removing the string carrier). Options: port declaration into `src/v3/std/resources.dag`, OR make `dsl/std/resources.dag` bootstrap-consumable by v3. Preferring the latter for single-authority. Separable from DB-15 implementation — can land independently. This is also a dissolution-of-dual-representation item; consider parking it in §Scheduled deletions if dsl/v3 duplication is the framing, or keep as a prerequisite deferral here. Preferring here for now since it's narrowly scoped.
+
+**Known v3-compiler gap surfaced during R2 impl (not blocking Stage 2c kickoff):** user-code construction of a record whose field is a `List<T>` rejects the empty-list literal (`requires: []`) with an "implicit template binding for `TestClaim` conflicts" diagnostic, even though the bootstrap-loaded `data` form accepts `field: []` cleanly. Today the Stage 2c smoke tests sidestep this by authoring non-empty `requires` lists; generated `TestClaim` data declarations (via `lens_testgen.rs`) continue to use `requires: []` because they go through the `data` form. The gap is orthogonal to DB-15 — it is a v3 type-inference limitation on user-code empty list literals — and is not gating the Stage 2c consumer runner work.
 
 ### Lane 2 Stage 2a / Track 17a boundary
 

src/v3/compiler/src/lens_testgen.rs

@@ -297,6 +297,16 @@ impl<'a> TestgenLens<'a> {
     ) {
         let declaration_name = format!("generated_test_claim_{:03}", *next_claim_id);
         *next_claim_id += 1;
+        // Every predicate variant this lens emits today (`Compiles`,
+        // `FailsWithDiagnostic`, `PortHasState`, `CostBounded`) is a
+        // compile-time assertion. Per DB-15 R2's per-claim `requires`
+        // convention (see `src/v3/std/verification.dag` §TestClaim
+        // docblock), compile-time claims carry the bootstrap-local
+        // sentinel `{ identifier: "compile_time" }` so downstream
+        // runners classify them correctly — an empty list is reserved
+        // for the post-resources-port dissolution window and would
+        // read as "no resources to acquire" rather than "compile-time
+        // only."
         claims.push(GeneratedClaim::new(
             self.dag,
             declaration_name,
@@ -314,6 +324,13 @@ impl<'a> TestgenLens<'a> {
                     FieldValue::Literal(LiteralBits::String(file_name)),
                 ),
                 ("predicate".to_string(), predicate),
+                (
+                    "requires".to_string(),
+                    FieldValue::List(vec![FieldValue::Record(vec![(
+                        "identifier".to_string(),
+                        FieldValue::Literal(LiteralBits::String("compile_time".to_string())),
+                    )])]),
+                ),
             ],
         ));
     }