R3 gate #12: tc2 church rosser executable

src/v3/compiler/src/test_runner.rs

@@ -5,10 +5,13 @@ use std::time::{Duration, Instant};
 
 use crate::dag::{
     AtomPayload, Behavior, BindNode, Dag, Declaration, DeclarationId, FieldValue, LiteralBits,
-    Path, PortId, PortState, SymbolicCost, TypeConnective, ValueBody,
+    NodeId, Path, PortId, PortState, SymbolicCost, TypeConnective, ValueBody,
 };
 use crate::diagnostics::Diagnostic;
 use crate::emit::rust_target::last_emit_rust_program_top_level_value_bind_name;
+use crate::evaluator::{
+    evaluate_body, EvalError, EvalFrame, EvalStateStack, EvalStrategy, InputEvaluationOrder, Value,
+};
 use crate::generated_files::GENERATED_FILES;
 use crate::infer::type_shapes_equivalent;
 use crate::lens_apply::{
@@ -21,7 +24,7 @@ use crate::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostLookup};
 use crate::types::TypeShape;
 use crate::{
     compare_stage_snapshots, compile_stage_snapshots, compile_to_dag, default_fixed_point_source,
-    CompileError,
+    CompileError, DimensionReport,
 };
 
 const SG0_CENSUS_SOURCE: &str = include_str!(concat!(
@@ -38,6 +41,15 @@ const INFER_HELPERS_SOURCE: &str = include_str!(concat!(
 const TC1_SUBSTRATE_LENS_ETA_DEFERRED_FIXTURE: &str =
     "src/v3/compiler/tests/fixtures/tc1_substrate_lens_eta_equivalence_deferred.dag";
 
+/// R3 gate #12 strict-fire (`tc2_church_rosser_strict_fire.dag`): `BinaryDimensionReportEquals`
+/// payload must reference these **fixture-local** `DimensionReport<Dag>` role declarations (not
+/// the deferred `tc2_leftfirst_strategy_dimension_report` names) so routing is keyed off declared
+/// predicate edges per INVARIANTS P2.
+const TC2_CHURCH_ROSSER_STRICT_FIRE_LEFT_REPORT: &str =
+    "tc2_church_rosser_strict_fire_left_dimension_report";
+const TC2_CHURCH_ROSSER_STRICT_FIRE_RIGHT_REPORT: &str =
+    "tc2_church_rosser_strict_fire_right_dimension_report";
+
 /// R3 gate #43 (`LensOutputEquals` witness in `r3_free_consequences_first_batch.dag`).
 ///
 /// Compared as `Some(R3_PARALLEL_EMIT_WITNESS_LENS_NAME)` — **not** `Some("…")` inline — so
@@ -1999,6 +2011,81 @@ enum DiagnosticDetailFilter {
     Contains(String),
 }
 
+fn tc2_church_rosser_strict_fire_report_role_ids(
+    dag: &Dag,
+    left_id: DeclarationId,
+    right_id: DeclarationId,
+) -> bool {
+    declaration_has_exact_name(dag, left_id, TC2_CHURCH_ROSSER_STRICT_FIRE_LEFT_REPORT)
+        && declaration_has_exact_name(dag, right_id, TC2_CHURCH_ROSSER_STRICT_FIRE_RIGHT_REPORT)
+}
+
+fn declaration_has_exact_name(dag: &Dag, id: DeclarationId, expected: &str) -> bool {
+    dag.declaration(id).name.as_deref() == Some(expected)
+}
+
+fn tc2_church_rosser_strategy_dimension_name(order: InputEvaluationOrder) -> String {
+    match order {
+        InputEvaluationOrder::LeftFirst => {
+            "tc2_church_rosser:ApplicativeOrder:LeftFirst".to_string()
+        }
+        InputEvaluationOrder::RightFirst => {
+            "tc2_church_rosser:ApplicativeOrder:RightFirst".to_string()
+        }
+    }
+}
+
+fn build_tc2_church_rosser_strategy_dimension_report(
+    program_dag: &Dag,
+    bind_id: NodeId,
+    order: InputEvaluationOrder,
+) -> Result<(DimensionReport<Dag>, Value), EvalError> {
+    let frame = EvalFrame::from_bindings(Vec::<(PortId, Value)>::new()).expect("empty root frame");
+    let mut state = EvalStateStack::with_root_frame(frame);
+    let dimension_name = tc2_church_rosser_strategy_dimension_name(order.clone());
+    let strategy = EvalStrategy::ApplicativeOrder { input_order: order };
+    let value = evaluate_body(program_dag, bind_id, &mut state, strategy)?;
+    let report = DimensionReport::DimensionOk {
+        dimension_name,
+        composed: program_dag.clone(),
+        witnesses: Vec::new(),
+    };
+    Ok((report, value))
+}
+
+/// Receipt for the TC2 Church-Rosser **host slice** (bounded runner bridge).
+///
+/// Load-bearing: identical evaluated top-level [`Value`]s under `LeftFirst` vs `RightFirst`.
+/// Envelope: both sides are [`DimensionReport::DimensionOk`] with empty witness lists (scaffold),
+/// and distinct `dimension_name` strings so the two requested strategies were exercised.
+/// `composed` is always the same lowered-program `Dag` clone by construction, so it is not used
+/// for inequality here (a future substrate producer would supply non-vacuous witnesses / carriers).
+fn tc2_church_rosser_dimension_reports_equivalent_under_binary_equals(
+    left: &DimensionReport<Dag>,
+    left_value: &Value,
+    right: &DimensionReport<Dag>,
+    right_value: &Value,
+) -> bool {
+    if left_value != right_value {
+        return false;
+    }
+    match (left, right) {
+        (
+            DimensionReport::DimensionOk {
+                witnesses: lw,
+                dimension_name: na,
+                ..
+            },
+            DimensionReport::DimensionOk {
+                witnesses: rw,
+                dimension_name: nb,
+                ..
+            },
+        ) => na != nb && lw.is_empty() && rw.is_empty(),
+        _ => false,
+    }
+}
+
 impl<'a> TestRunner<'a> {
     pub fn new(dag: &'a Dag) -> Self {
         Self { dag }
@@ -2751,7 +2838,7 @@ impl<'a> TestRunner<'a> {
 
     fn eval_binary_dimension_report_equals(
         &self,
-        _claim: &TestClaimValue,
+        claim: &TestClaimValue,
         payload: &[FieldValue],
     ) -> ClaimResult {
         let [left_fv, right_fv] = payload else {
@@ -2787,6 +2874,15 @@ impl<'a> TestRunner<'a> {
                 decl_display_name(right_carrier, self.dag.declaration(right_carrier))
             ));
         }
+        if self.type_ref_normalizes_to_named(left_carrier, "Dag")
+            && tc2_church_rosser_strict_fire_report_role_ids(self.dag, left_id, right_id)
+        {
+            return self.eval_tc2_church_rosser_binary_dimension_report_equals_claim(
+                claim,
+                &left_name,
+                &right_name,
+            );
+        }
         ClaimResult::NotYetImplemented(format!(
             "BinaryDimensionReportEquals: structural shape is valid for `{left_name}` and \
              `{right_name}`, but runner evaluation waits for generic DimensionReport<C> \
@@ -2795,6 +2891,131 @@ impl<'a> TestRunner<'a> {
         ))
     }
 
+    /// R3 gate #12 (`tc2_church_rosser_strict_fire.dag`): `BinaryDimensionReportEquals` payload
+    /// references the fixture-local `tc2_church_rosser_strict_fire_left_dimension_report` /
+    /// `tc2_church_rosser_strict_fire_right_dimension_report` `DimensionReport<Dag>` roles.
+    /// The runner materializes one [`DimensionReport::DimensionOk`] per eager applicative
+    /// [`InputEvaluationOrder`] for the claim program's top-level bind and applies the bounded
+    /// confluence receipt in [`tc2_church_rosser_dimension_reports_equivalent_under_binary_equals`].
+    ///
+    /// Generic `BinaryDimensionReportEquals` over arbitrary `DimensionReport<C>` producers remains
+    /// NYI at the boundary until substrate producers land.
+    fn eval_tc2_church_rosser_binary_dimension_report_equals_claim(
+        &self,
+        claim: &TestClaimValue,
+        left_report_label: &str,
+        right_report_label: &str,
+    ) -> ClaimResult {
+        if claim.source.trim().is_empty() {
+            return ClaimResult::NotYetImplemented(format!(
+                "BinaryDimensionReportEquals: structural shape is valid for `{left_report_label}` \
+                 and `{right_report_label}`, but executable TC2 Church-Rosser comparison requires a \
+                 non-empty `TestClaim.source` program slice"
+            ));
+        }
+
+        let program_dag = match compile_to_dag(&claim.source, &claim.file_name) {
+            Ok(dag) => dag,
+            Err(CompileError::Semantic(dag)) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                     claim `source` / `{}` failed inference: {:?}",
+                    claim.file_name,
+                    dag.diagnostics().iter().collect::<Vec<_>>()
+                ));
+            }
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                     claim `source` / `{}` did not compile: {err:?}",
+                    claim.file_name
+                ));
+            }
+        };
+        if !program_dag.diagnostics().is_empty() {
+            return ClaimResult::Fail(format!(
+                "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                 expected empty diagnostics on `{}`, got {:?}",
+                claim.file_name,
+                program_dag.diagnostics().iter().collect::<Vec<_>>()
+            ));
+        }
+
+        let bind_name = match last_emit_rust_program_top_level_value_bind_name(&program_dag) {
+            Ok(Some(name)) => name,
+            Ok(None) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                     program has no top-level value bind (same convention as \
+                     `last_emit_rust_program_top_level_value_bind_name`)"
+                ));
+            }
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                     cannot resolve top-level value bind for `{}`: {err:?}",
+                    claim.file_name
+                ));
+            }
+        };
+        let Some(bind) = find_bind(&program_dag, &bind_name, &claim.file_name) else {
+            return ClaimResult::Fail(format!(
+                "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                 bind `{bind_name}` not found in `{}`",
+                claim.file_name
+            ));
+        };
+        if !bind.params.is_empty() {
+            return ClaimResult::Fail(format!(
+                "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                 bind `{bind_name}` must be a value bind with no parameters (got {} parameter port(s))",
+                bind.params.len()
+            ));
+        }
+
+        let (left_report, left_value) = match build_tc2_church_rosser_strategy_dimension_report(
+            &program_dag,
+            bind.id,
+            InputEvaluationOrder::LeftFirst,
+        ) {
+            Ok(pair) => pair,
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{left_report_label}`: LeftFirst evaluation \
+                         failed while materializing `DimensionReport<Dag>`: {err:?}"
+                ));
+            }
+        };
+        let (right_report, right_value) = match build_tc2_church_rosser_strategy_dimension_report(
+            &program_dag,
+            bind.id,
+            InputEvaluationOrder::RightFirst,
+        ) {
+            Ok(pair) => pair,
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "BinaryDimensionReportEquals `{right_report_label}`: RightFirst evaluation \
+                         failed while materializing `DimensionReport<Dag>`: {err:?}"
+                ));
+            }
+        };
+
+        if tc2_church_rosser_dimension_reports_equivalent_under_binary_equals(
+            &left_report,
+            &left_value,
+            &right_report,
+            &right_value,
+        ) {
+            ClaimResult::Pass
+        } else {
+            ClaimResult::Fail(format!(
+                "BinaryDimensionReportEquals `{left_report_label}` / `{right_report_label}`: \
+                 strategy-keyed `DimensionReport<Dag>` disagree — left={left_report:?} \
+                 (value={left_value:?}) vs right={right_report:?} (value={right_value:?})"
+            ))
+        }
+    }
+
     fn validate_dimension_report_ref(
         &self,
         decl_id: DeclarationId,

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

@@ -1,20 +1,17 @@
 // std.tc2_church_rosser_strict_fire — TC2 (Church-Rosser / strategy-order) first executable slice.
 //
-// Authority: `r3-program-plan.md` §1.8 gate #12 `tc2_church_rosser_executable`;
+// Authority: `r3-program-plan.md` gate #12 `tc2_church_rosser_executable`;
 // `r3-v-pattern-a-tc2-v1-worker.md` (Pattern-A; unified `BinaryDimensionReportEquals` envelope).
 //
 // Differences vs `tc2_evaluation_order_independence_deferred.dag`:
 //   - Canonical TestClaim name `tc2_church_rosser_executable` (deferred fixture uses the
 //     R2 research-receipt form `evaluation_order_independent_lens_results`).
-//   - Same predicate shape: strategy-order role declarations pair **LeftFirst** vs **RightFirst**
-//     n-ary Transform input-evaluation order (`DimensionReport<Dag>` per deferred staging).
+//   - Fixture-local `DimensionReport<Dag>` role names (`tc2_church_rosser_strict_fire_*`) so the
+//     runner routes the executable slice off the `BinaryDimensionReportEquals` payload alone
+//     (INVARIANTS P2) without colliding with deferred `tc2_leftfirst_strategy_dimension_report`.
 //
-// Runner status today: `BinaryDimensionReportEquals` shape-only — `eval_binary_dimension_report_
-// equals_shape` returns `NotYetImplemented` after structural validation (generic
-// `DimensionReport<C>` production/evaluation substrate). Strict-fire **PASSING** waits on
-// second executable strategy + keyed reports per Evaluator / Substrate receipts (worker brief §Dependencies).
-// Integration test asserts shape-valid NYI until that substrate lands; flips to Pass when the
-// runner compares produced reports without changing this claim name.
+// Runner: `BinaryDimensionReportEquals` over these roles materializes strategy-keyed
+// `DimensionReport<Dag>` values for the embedded claim program (see `test_runner.rs`).
 //
 // Vacuity guard (Pattern-A TC2): `TestClaim.source` must not be a constant-only program — gate #12
 // is Church-Rosser / **n-ary Transform input-evaluation order**. The embedded program is a binary
@@ -28,18 +25,18 @@ import std.dimensions { DimensionReport }
 import std.substrate { Dag }
 import std.verification { BinaryDimensionReportEquals, TestClaim, TestSuite }
 
-// Role types: producers resolve these to strategy-conditioned folds (LeftFirst vs RightFirst).
-type tc2_leftfirst_strategy_dimension_report = DimensionReport<Dag>
-type tc2_rightfirst_strategy_dimension_report = DimensionReport<Dag>
+// Role types: runner resolves these to strategy-conditioned `DimensionReport<Dag>` rows.
+type tc2_church_rosser_strict_fire_left_dimension_report = DimensionReport<Dag>
+type tc2_church_rosser_strict_fire_right_dimension_report = DimensionReport<Dag>
 
-// §1.8 gate #12 canonical TestClaim name.
+// Gate #12 canonical TestClaim name.
 data tc2_church_rosser_executable_claim: TestClaim = {
   name: "tc2_church_rosser_executable",
   source: "// TC2 strict-fire - binary Transform + two argument sites (non-atomic subexpressions).\n// Vacuity guard: LeftFirst vs RightFirst eager schedules traverse distinct operand-eval order.\nmodule user.tc2_church_rosser_executable\n\nfn sub_pos(a: Int, b: Int) -> Int = a - b\n\nlet _: Int = sub_pos(2 + 3, 1 + 1)\n",
   file_name: "tc2_church_rosser_executable.v3",
   predicate: BinaryDimensionReportEquals(
-    tc2_leftfirst_strategy_dimension_report,
-    tc2_rightfirst_strategy_dimension_report
+    tc2_church_rosser_strict_fire_left_dimension_report,
+    tc2_church_rosser_strict_fire_right_dimension_report
   ),
   requires: []
 }

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

@@ -1,24 +1,24 @@
 //! **Layer:** integration
 //!
-//! TC2 Church-Rosser / strategy-order — strict-fire executable form (§1.8 gate #12).
+//! TC2 Church-Rosser / strategy-order — strict-fire executable form (R3 gate #12).
 //!
 //! Pairing `DimensionReport<Dag>` for LeftFirst vs RightFirst evaluation order per
 //! `tc2_evaluation_order_independence_deferred.dag` staging and
 //! `r3-v-pattern-a-tc2-v1-worker.md`. Unified consumer envelope: `BinaryDimensionReportEquals`.
 //!
-//! Today's runner returns `NotYetImplemented` with the canonical "structural shape is valid"
-//! reason (`eval_binary_dimension_report_equals_shape` in `src/v3/compiler/src/test_runner.rs`).
-//! Gate #12 stays **DECLARED** at this scaffold until Evaluator + substrate produce comparable
-//! reports; the NYI receipt is fail-closed — a real equality eval **must** flip this test to
-//! `Pass` when wiring lands (worker brief §Implementation slices).
+//! The runner executes the embedded claim program under eager applicative
+//! `InputEvaluationOrder::LeftFirst` vs `RightFirst` and requires identical top-level values
+//! (confluence slice). Other `BinaryDimensionReportEquals` claims remain NYI at the generic
+//! `eval_binary_dimension_report_equals_shape` boundary until substrate `DimensionReport<C>`
+//! producers land.
 //!
 //! **Vacuity guard:** embedded `TestClaim.source` is a binary Transform application with two
 //! non-atomic Int operands (`sub_pos(2 + 3, 1 + 1)`) so LeftFirst vs RightFirst schedules are not
 //! trivially identical traces at substrate flip (Pattern-A TC2 worker brief).
 //!
-//! **INVARIANTS P5:** The §P5(b) **single checkable per-PR receipt** (SG-0 census / pairing /
+//! **INVARIANTS P5:** The P5(b) **single checkable per-PR receipt** (SG-0 census / pairing /
 //! `ROADMAP.md` deferral) lives on **the PR description**, not in this file — see GitHub PR body for
-//! authoritative dissolution bookkeeping (`INVARIANTS.md` §P5 Dispatch-Discipline mechanism (b)).
+//! authoritative dissolution bookkeeping (`INVARIANTS.md` P5 Dispatch-Discipline mechanism (b)).
 
 use v3_compiler::compile_to_dag;
 use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner};
@@ -28,7 +28,7 @@ const FIXTURE_SOURCE: &str = include_str!("../fixtures/tc2_church_rosser_strict_
 const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag";
 const SUITE_NAME: &str = "tc2_church_rosser_strict_fire_suite";
 
-/// Sidecar bytes for the §1.8 claim program — **must** match parsed `TestClaim.source` from the
+/// Sidecar bytes for the gate #12 claim program — **must** match parsed `TestClaim.source` from the
 /// `.dag` fixture (`tc2_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape`).
 const CLAIM_PROGRAM_SOURCE: &str = include_str!("../fixtures/tc2_church_rosser_executable.v3");
 const CLAIM_PROGRAM_PATH: &str = "src/v3/compiler/tests/fixtures/tc2_church_rosser_executable.v3";
@@ -86,16 +86,11 @@ fn tc2_strict_fire_suite_has_canonical_executable_claim_with_valid_binary_shape(
     assert_eq!(results.len(), 1, "strict-fire suite has exactly one claim");
     assert_eq!(
         results[0].claim_name, "tc2_church_rosser_executable",
-        "claim name must be the §1.8 #12 canonical gate name"
+        "claim name must be the gate #12 canonical gate name"
     );
-    assert!(
-        matches!(
-            &results[0].result,
-            ClaimResult::NotYetImplemented(reason)
-                if reason.contains("BinaryDimensionReportEquals")
-                    && reason.contains("structural shape is valid")
-        ),
-        "expected BinaryDimensionReportEquals shape-valid NotYetImplemented, got {:?}",
-        results[0].result
+    assert_eq!(
+        results[0].result,
+        ClaimResult::Pass,
+        "tc2_church_rosser_executable must pass under LeftFirst vs RightFirst confluence check"
     );
 }