docs(evaluator): PR-D slice 0 — cross-target harness brief + TestClaim hook

docs/briefs/r2-evaluator-manager.md

@@ -28,7 +28,7 @@ R2's Goal 7 — **Runtime evaluator for `.dag` programs**. The Evaluator is the
 | **Body evaluator** | L | NOT YET AUTHORED — gated on Runtime value model | Execute `.dag` function bodies structurally. Bounded forward execution per INVARIANTS P4. Termination by descent evidence (already in substrate per `dsl/std/termination.dag`). |
 | **Lens application** | M | OPEN — complete reflection **landed** (#1170); **PR-E slice 1 landed** — `fold_lens_over_reflected_program` wires reflect → prepend carrier → `apply_lens_declaration` on one `lens_program` ([`docs/briefs/r2-pr-e-lens-application-over-reflected-program-dag.md`](r2-pr-e-lens-application-over-reflected-program-dag.md)) | `reflect_program_dag_nodes_in_file` is structurally complete per [design-reflection completeness](../design-reflection-completeness.md) §"Decision". **Lens application** sub-lane stays **OPEN** for full `Lens<C>` / `DimensionReport` / PB-Runtime fold semantics over that spine; slice 1 is the bounded **reflect+apply** seam only (deeper carriers: PR-E brief + Worker A). |
 | **Witness construction** | M | NOT YET AUTHORED | Runtime materialization of proof artifacts (`Witness::Inhabits` / `Witness::Violates` per `src/v3/std/dimensions.dag`); algebraic-law witnesses (associativity, commutativity, identity). |
-| **Cross-target equivalence harness primitives** | S | NOT YET AUTHORED | For L5 verification in R3 (algebraic equivalence over a curated corpus, per #1078 design challenge #3 locked decision). Primitives only — corpus authoring is post-R2 (R3 lane T-Verification-L5-Corpus). |
+| **Cross-target equivalence harness primitives** | S | **PR-D slice 0 opened** — named `.dag` `TestClaim` + suite ([`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md)); L5-shaped multi-target receipts deferred on LanguageSpec + Shape A grounding (brief §Dependencies). | For L5 verification in R3 (algebraic equivalence over a curated corpus, per #1078 design challenge #3 locked decision). Primitives only — corpus authoring is post-R2 (R3 lane T-Verification-L5-Corpus). |
 
 ## Pre-dispatch design lock cadence (per #1078 locked structure)
 
@@ -53,7 +53,7 @@ Before worker dispatch begins on the implementation sub-lanes above, **5 design
 | **PR-A** | (foundational) | — | Runtime value model — closed-over environments, lazy/eager strategy, memoization | NOT YET AUTHORED |
 | **PR-B** | PR-A | PR-C, PR-D | Witness construction surface — concrete shape for runtime materialization | NOT YET AUTHORED |
 | **PR-C** | (foundational; substrate-reflection-shape) | PR-A, PR-B, PR-D | Reflection completeness spec — what does "complete reflection" mean for `reflect_program_dag_nodes_in_file`? | **LANDED via #1129** at [`docs/design-reflection-completeness.md`](../design-reflection-completeness.md) (consumed by R3-T-LensProducer-Retirement per §"Cascade and gates") |
-| **PR-D** | (foundational; cross-target spec) | PR-A, PR-B, PR-C | L5 corpus type spec — algebraic equivalence over curated corpus (locked direction; specific design here) | NOT YET AUTHORED (consumed by R3-T-V-L5-Corpus) |
+| **PR-D** | (foundational; cross-target spec) | PR-A, PR-B, PR-C | L5 corpus type spec — algebraic equivalence over curated corpus (locked direction; specific design here) | **Slice 0 opened** — worker brief [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) + structural `TestClaim` hook (consumed by R3-T-V-L5-Corpus); strict cross-target predicates follow LanguageSpec / grounding deps in that brief |
 | **PR-E** | All of PR-A through PR-D | (synthesis; serializes after) | Final integration design — synthesizes PR-A through PR-D into the implementation roadmap | NOT YET AUTHORED |
 
 **Sequencing principle (per Director directive 2026-04-28):** "focus on dependencies — writing code is fast; we get stuck in review." Parallelize PR-A, PR-C, PR-D as independent foundational design locks; PR-B serializes after PR-A (witness construction uses runtime values); PR-E synthesizes after all four. Worker dispatch on implementation sub-lanes blocks on PR-E.
@@ -127,7 +127,7 @@ Each sub-lane closes under a structural acceptance gate authored as a `.dag` `Te
 - `evaluator_body_evaluator_correctly_executes_std_termination` — Body evaluator correctly executes `dsl/std/termination.dag` body programs (representative test)
 - `evaluator_lens_application_complete_reflection` — `reflect_program_dag_nodes_in_file` returns complete reflection (no shallow/lossy gaps) per [`docs/design-reflection-completeness.md`](../design-reflection-completeness.md) §"Decision" (5.1-5.3 sub-questions resolved). **Structural `.dag` claim hook (named target):** add `data evaluator_lens_application_complete_reflection: TestClaim = …` to `src/v3/compiler/tests/fixtures/r2_evaluator_lens_application.template.dag` when R2 gate splices land (see [`docs/briefs/r2-pr-e-lens-application-over-reflected-program-dag.md`](r2-pr-e-lens-application-over-reflected-program-dag.md) §Acceptance hook).
 - `evaluator_witness_construction_per_lens_correct` — runtime witness materialization correct for at least 3 lens instances (complexity / tenant-flow / IFC per design-lens-framework.md)
-- `evaluator_cross_target_equivalence_harness_primitives_landed` — primitives ready for R3-T-V-L5-Corpus consumer (no corpus authoring at R2; primitives only)
+- `evaluator_cross_target_equivalence_harness_primitives_landed` — primitives ready for R3-T-V-L5-Corpus consumer (no corpus authoring at R2; primitives only). **Structural `.dag` claim hook (named target):** `data evaluator_cross_target_equivalence_harness_primitives_landed: TestClaim = …` in [`src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag`](../../src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag) (suite `r2_evaluator_cross_target_equivalence_harness_primitives_suite`; slice 0 predicate `Compiles` — see [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) §Next implementation slices).
 
 **Plus:** `lens_complexity_n_log_n_fold_correct` + `lens_tenant_flow_aggregate_validate_fail_closed` + `lens_ifc_aggregate_validate_fail_closed` (TestClaims from `docs/design-lens-framework.md` I4 + I9).
 
@@ -139,7 +139,7 @@ Each sub-lane closes under a structural acceptance gate authored as a `.dag` `Te
 - PR-A worker brief — Runtime value model design lock
 - PR-B worker brief — Witness construction surface design lock
 - ~~PR-C worker brief — Reflection completeness spec~~ — **LANDED via #1129** at [`docs/design-reflection-completeness.md`](../design-reflection-completeness.md)
-- PR-D worker brief — L5 corpus type spec
+- ~~PR-D worker brief — L5 corpus type spec~~ — **slice 0 opened** in [`docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md) (this PR; strict L5 multi-target harness: follow §Next implementation slices in that brief)
 - PR-E worker brief — Final integration design synthesis
 - Implementation worker briefs (one per sub-lane: runtime value model implementation, body evaluator implementation, lens application implementation, witness construction implementation, cross-target equivalence primitives)
 - **PR-E lens-application fold (slice 1 landed; deeper fold in flight)** — [`docs/briefs/r2-pr-e-lens-application-over-reflected-program-dag.md`](r2-pr-e-lens-application-over-reflected-program-dag.md); `fold_lens_over_reflected_program` in `src/v3/compiler/src/lens_apply.rs` runs **reflect → `apply_lens_declaration`** (single `lens_program` authority; reflected carrier as first lens arg). Deeper `Lens<C>` / `DimensionReport` / PB-Runtime + Worker A boundaries remain open per that brief.

docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md

@@ -0,0 +1,46 @@
+# PR-D — Cross-target equivalence harness primitives (Evaluator Manager)
+
+**Status:** PROPOSAL — **slice 0 (this PR)** opens the named `TestClaim` + runner-visible suite hook (`evaluator_cross_target_equivalence_harness_primitives_landed` / suite in §Structural acceptance); deeper harness surfaces deferred with explicit dependencies below. Use **landed** in manager-brief consumption rows only **after** this PR merges (keeps open-PR status language honest).
+
+**Parent:** [`docs/briefs/r2-evaluator-manager.md`](r2-evaluator-manager.md) — sub-lane **Cross-target equivalence harness primitives** + design-lock row **PR-D**.
+
+**R3 consumer:** [`docs/r3-structure.md`](../r3-structure.md) — **T-Verification-L5-Corpus** acceptance `l5_cross_target_consistency` (Rust / Python / Go equivalent runtime behavior on the certification corpus). R2 lands **primitives only**; corpus authoring stays R3.
+
+## Scope (this PR-D program)
+
+1. **Harness contract (R2):** a stable, named structural gate `evaluator_cross_target_equivalence_harness_primitives_landed` so R3 Verification Manager can depend on a single fixture path without inventing parallel claim names.
+2. **Primitives, not corpus:** stub programs and `std.verification` `TestPredicate` variants **already declared** on substrate (`Compiles` for slice 0; **scaffold** variants `ForAllTargets` / `LensOutputEquals` / `DifferentialEquals` at `src/v3/std/verification.dag` ~L147–L181 — each marked 🟡 in-file with a dissolution comment). **Strict L5-shaped harness rows** (multi-target emit/eval parity, certification corpus) remain **ungated until §Dependencies** — this brief does not treat those receipts as grounded. No curated L5 corpus rows at R2.
+3. **Algebraic equivalence framing:** L5 compares **computational results** across targets (per `r3-structure.md`), not byte identity. PR-D does not introduce new `TestPredicate` variants — substrate introduction is [`INVARIANTS.md`](../../INVARIANTS.md) §P1 / Grounding Manager only if a **future** fact cannot be expressed even after the existing sum + runner wiring is exercised.
+
+## Explicitly out of scope (Worker A / PR-A / PB-Runtime)
+
+- **Runtime `Value` / `EvalFrame` / closed-over environments** — Evaluator PR-A + PB-Runtime §3.2–§3.3 in [`docs/design-pb-runtime-interpreter.md`](../design-pb-runtime-interpreter.md). PR-D harness receipts must not smuggle runtime-value design; cross-target comparison stays at “compile + emit + observe” boundaries the **existing** predicates already model (`ForAllTargets` scaffold, etc.).
+- **Full `fold_lens<C>` / `DimensionReport<C>`** over emitted artifacts — lens consumer shape in [`docs/design-lens-framework.md`](../design-lens-framework.md); L4/L7 harness semantics in `r3-structure.md` §lane table. PR-D does not replace T-Verification-L4-L7-Direct.
+
+## Dependencies (blockers for “strict” L5-shaped slices)
+
+| Dependency | Why |
+|---|---|
+| **R2-T-Ground-LanguageSpec** (parallel lane) | Per-target primitive realization + typed capability edges for comparable observations across Rust / Python / Go. |
+| **All three Shape A targets grounded** | `l5_cross_target_consistency` requires emit paths for each target on the same `Dag` (see `r3-structure.md` T-Verification-L5-Corpus row). |
+| **T-Verification-L4-L7-Direct corpus exists** | R3 critical path: Direct seeds L5 coverage suite. |
+
+Until those land, **slice 0** is intentionally thin: the named `TestClaim` wires through `TestRunner` with `Compiles` on a minimal witness program so CI exercises the same compilation path future `DifferentialEquals` / per-target receipts will attach to.
+
+## Structural acceptance — `.dag` hook (authoritative path)
+
+| Gate name | Fixture | Suite `name` |
+|---|---|---|
+| `evaluator_cross_target_equivalence_harness_primitives_landed` | [`src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag`](../../src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag) | `r2_evaluator_cross_target_equivalence_harness_primitives_suite` |
+
+**Deferred fixture path (if this file moves):** keep the **declaration name** `evaluator_cross_target_equivalence_harness_primitives_landed` stable; update only the module `std.r2_evaluator_cross_target_equivalence_harness_primitives` path in one PR with Evaluator Manager brief + integration test `include_str!` path co-updated.
+
+## Next implementation slices (ordered)
+
+1. **Slice 1 — oracle stub pair:** second `TestClaim` in the same module using the **existing** `TestPredicate::DifferentialEquals` constructor (substrate sum at `verification.dag`; runner: Lane-E / `test_runner.rs`) with subject/oracle both on trivial `.dag`-expressible functions — proves this fixture file is the home for differential receipts **without** multi-target emit. **Does not** require new `TestPredicate` variants; blocked only if runner/regression gaps surface (then §P1), not because the constructor is absent.
+2. **Slice 2 — emit-scoped receipt:** once §Dependencies (LanguageSpec + Shape A targets) are ready, add a claim using the **existing** `TestPredicate::ForAllTargets` constructor **only** if Director-approved for this fixture (same release-deferral discipline as other scaffold uses); otherwise keep deferral documented here and in manager brief. **Does not** assert `ForAllTargets` is absent from substrate — only that **using** it for real cross-target evidence waits on emit infra + approval.
+3. **Slice 3 — R3 handoff doc:** one paragraph in Verification Manager spawn brief naming `r2_evaluator_cross_target_equivalence_harness_primitives.dag` as the structural import surface for `l5_cross_target_consistency` corpus wiring.
+
+## Dissolution
+
+When `l5_cross_target_consistency` is fully expressible as strict `TestClaim` rows on the certification corpus with no `Compiles`-only stub, delete or downgrade the stub source inside `evaluator_cross_target_equivalence_harness_primitives_landed` to match the strict predicate — do not delete the **claim name** without a Director-amended acceptance table in `r2-evaluator-manager.md`.

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

@@ -0,0 +1,22 @@
+// std.r2_evaluator_cross_target_equivalence_harness_primitives — PR-D (Evaluator Manager).
+//
+// Structural acceptance hook: `evaluator_cross_target_equivalence_harness_primitives_landed`
+// per docs/briefs/r2-evaluator-manager.md §Acceptance. Slice 0 uses `Compiles` only; see
+// docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md for deferred L5-shaped work.
+
+module std.r2_evaluator_cross_target_equivalence_harness_primitives
+
+import std.verification { Compiles, TestClaim, TestSuite }
+
+data evaluator_cross_target_equivalence_harness_primitives_landed: TestClaim = {
+  name: "evaluator_cross_target_equivalence_harness_primitives_landed",
+  source: "fn trivial_identity(x: Int) -> Int = x\nlet _: Int = trivial_identity(0)\n",
+  file_name: "r2_pr_d_harness_primitive_stub.v3",
+  predicate: Compiles,
+  requires: []
+}
+
+data r2_evaluator_cross_target_equivalence_harness_primitives_suite: TestSuite = {
+  name: "r2_evaluator_cross_target_equivalence_harness_primitives_suite",
+  claims: [evaluator_cross_target_equivalence_harness_primitives_landed]
+}

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

@@ -1,5 +1,6 @@
 use v3_compiler::compile_to_dag;
 use v3_compiler::dag::{Behavior, Dag, DeclarationId, PortState, TypeConnective};
+use v3_compiler::test_runner::{ClaimResult, TestRunner};
 use v3_compiler::CompileError;
 
 fn compile_any(src: &str, file: &str) -> Dag {
@@ -323,3 +324,39 @@ let suite: TestSuite = {
         find_named(&dag, "TestSuite")
     );
 }
+
+/// PR-D (Evaluator Manager): cross-target equivalence harness — named structural gate
+/// `evaluator_cross_target_equivalence_harness_primitives_landed` compiles and passes `Compiles`
+/// under `TestRunner` (see `docs/briefs/r2-pr-d-cross-target-equivalence-harness-primitives.md`).
+const R2_PR_D_HARNESS_FIXTURE: &str =
+    include_str!("../fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag");
+const R2_PR_D_HARNESS_FIXTURE_PATH: &str =
+    "src/v3/compiler/tests/fixtures/r2_evaluator_cross_target_equivalence_harness_primitives.dag";
+
+#[test]
+fn r2_pr_d_cross_target_equivalence_harness_primitives_suite_passes() {
+    let dag = match compile_to_dag(R2_PR_D_HARNESS_FIXTURE, R2_PR_D_HARNESS_FIXTURE_PATH) {
+        Ok(dag) => {
+            assert!(
+                dag.diagnostics().is_empty(),
+                "{R2_PR_D_HARNESS_FIXTURE_PATH}: expected empty module diagnostics, got {:?}",
+                dag.diagnostics().iter().collect::<Vec<_>>()
+            );
+            dag
+        }
+        Err(CompileError::Semantic(dag)) => panic!(
+            "{R2_PR_D_HARNESS_FIXTURE_PATH} should lower without module diagnostics. Got `Err(Semantic)`: {:?}",
+            dag.diagnostics().iter().collect::<Vec<_>>()
+        ),
+        Err(other) => panic!("unexpected compile error for {R2_PR_D_HARNESS_FIXTURE_PATH}: {other:?}"),
+    };
+
+    let results = TestRunner::new(&dag)
+        .run_suite("r2_evaluator_cross_target_equivalence_harness_primitives_suite");
+    assert_eq!(results.len(), 1);
+    assert_eq!(
+        results[0].claim_name,
+        "evaluator_cross_target_equivalence_harness_primitives_landed"
+    );
+    assert_eq!(results[0].result, ClaimResult::Pass);
+}