R3 gate #51: BinaryDimensionReportEquals constant-fold witness (#2575)

docs/r3-program-plan.md

@@ -274,7 +274,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 48 | `auto_loop_parallelism_dependence_emits_sequential` | demonstration | T-Free-Consequences-Demonstration | DECLARED | provable dependence → sequential |
 | 49 | `auto_memoization_repeated_pure_call_cached` | demonstration | T-Free-Consequences-Demonstration | DECLARED | composes Lens<Purity>·Lens<Cost> |
 | 50 | `auto_memoization_no_caching_for_one_shot` | demonstration | T-Free-Consequences-Demonstration | DECLARED | no scaffolding for single-call |
-| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | DECLARED | structural cost-shrink across targets |
+| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | **CONSUMER_LANDED (partial)** — #2577: `SymbolicCostExprEquals` baseline on `main`; issue **#2575** / branch `session/smart-cat-457`: representative `fold_pre` / `fold_post` + `TestRunner` executable `BinaryDimensionReportEquals` (Int-add `OperatorRealization` + cross-target `Type(Int)` overlay). **Not** `r3-structure.md` certification-corpus-wide closure; **PASSING** stays deferred until that bar is evidenced. | structural cost-shrink across targets |
 | 52 | `cross_target_optimization_cost_structurally_derived` | structural-fold | T-Free-Consequences-Demonstration | DECLARED | cost-lens reading structurally derived |
 | 53 | `workflow_substrate_carriers_landed` | substrate-shape | T-Workflow-As-Data | **CONSUMER_LANDED (partial)** (PR #2160 — WorkflowSecret + CronExpression β-ratified; refresh per cluster-analysis audit §1; remaining sub-carriers tracked in T-WAD slice queue) | `std.workflow` carriers |
 | 54 | `timing_lens_carrier_landed` | substrate-shape | T-Workflow-As-Data | **CONSUMER_LANDED** (PR #2360 — Substrate T-Workflow-As-Data timing-lens carrier post-T-LBP COMPLETE) | `Lens<TimingMeasurement>` carrier |

src/v3/compiler/src/test_runner.rs

@@ -5,7 +5,7 @@ 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;
@@ -1999,6 +1999,143 @@ enum DiagnosticDetailFilter {
     Contains(String),
 }
 
+fn find_named_bind_workflow_root(dag: &Dag, bind_name: &str) -> Result<NodeId, String> {
+    dag.nodes()
+        .iter()
+        .find(|behavior| behavior.as_bind().is_some_and(|bind| bind.name == bind_name))
+        .map(Behavior::id)
+        .ok_or_else(|| {
+            format!(
+                "BinaryDimensionReportEquals gate #51 (`cross_target_optimization_constant_fold_consistent`): \
+                 claim `TestClaim.source` must declare top-level bind `{bind_name}` for the cost witness surface"
+            )
+        })
+}
+
+/// R3 gate #51 — `BinaryDimensionReportEquals` consumer surface.
+///
+/// `fold_pre` / `fold_post` are **different** workflow roots (pre-fold `1 + 2` vs literal `3`).
+/// Full `DimensionReport` witness-vector equality is intentionally not required (different backward
+/// slices). The behavioral contract is:
+/// 1. Both reports are [`crate::DimensionReport::DimensionOk`].
+/// 2. `normalize(sequential(composed_post, Constant(delta))) == normalize(composed_pre)` where
+///    `delta` is the **LanguageSpec** `OperatorRealization` cost for `Int` addition, and the same
+///    `delta` is verified across rust/python/go (cross-target structural agreement on the folded
+///    surface).
+/// 3. Caller then checks the cross-target `Type(Int)` overlay on the shared normalized bound.
+fn gate51_constant_fold_pre_post_reports_align(
+    bootstrap: &Dag,
+    pre: &crate::DimensionReport<SymbolicCost>,
+    post: &crate::DimensionReport<SymbolicCost>,
+) -> Result<(), String> {
+    use crate::dag::{normalize, sequential};
+    use crate::realization_cost::{RealizationCostKey, RealizationCostTable};
+    use crate::DimensionReport;
+
+    let (dimension_name, pre_composed, post_composed) = match (pre, post) {
+        (
+            DimensionReport::DimensionOk {
+                dimension_name: pn,
+                composed: pc,
+                ..
+            },
+            DimensionReport::DimensionOk {
+                dimension_name: qn,
+                composed: qc,
+                ..
+            },
+        ) => {
+            if pn != qn {
+                return Err(format!(
+                    "gate #51 `dimension_name` mismatch between `fold_pre` and `fold_post` roots: \
+                     {pn:?} vs {qn:?}"
+                ));
+            }
+            (pn.clone(), pc.clone(), qc.clone())
+        }
+        _ => {
+            return Err(format!(
+                "gate #51 requires `DimensionOk` on both `fold_pre` and `fold_post` workflow roots; \
+                 pre={pre:?}; post={post:?}"
+            ));
+        }
+    };
+
+    let int_decl = bootstrap
+        .declaration_by_name("Int")
+        .map(|d| d.id)
+        .ok_or_else(|| "bootstrap missing `Int` declaration for gate #51".to_string())?;
+
+    let mut int_add_cost: Option<i64> = None;
+    for (lang_name, row_name) in [
+        ("rust_language", "rust_int_add"),
+        ("python_language", "python_int_add"),
+        ("go_language", "go_int_add"),
+    ] {
+        let op = realization_row_op_decl(bootstrap, row_name)?;
+        let lang_id = bootstrap
+            .declaration_by_name(lang_name)
+            .map(|d| d.id)
+            .ok_or_else(|| format!("bootstrap missing `{lang_name}` for gate #51"))?;
+        let table = RealizationCostTable::for_language(bootstrap, lang_id)
+            .map_err(|e| format!("RealizationCostTable({lang_name}) for gate #51: {e:?}"))?;
+        let Some(entry) = table.get(&RealizationCostKey::Operator {
+            target: int_decl,
+            op,
+        }) else {
+            return Err(format!(
+                "gate #51: `{lang_name}` realization table missing Operator(Int,+) row (via `{row_name}`)"
+            ));
+        };
+        let c = entry.cost.value();
+        match int_add_cost {
+            None => int_add_cost = Some(c),
+            Some(prev) if prev != c => {
+                return Err(format!(
+                    "gate #51: Int add realization `cost` differs cross-target (`{row_name}`): {prev} vs {c}"
+                ));
+            }
+            Some(_) => {}
+        }
+    }
+
+    let delta =
+        int_add_cost.ok_or_else(|| "gate #51: missing Int add realization cost".to_string())?;
+    let adjusted_post = normalize(sequential(
+        post_composed,
+        SymbolicCost::ConstantCost { _0: delta },
+    ));
+    let pre_norm = normalize(pre_composed);
+    if adjusted_post != pre_norm {
+        return Err(format!(
+            "gate #51 structural constant-fold witness failed (dimension={dimension_name}): expected \
+             normalize(sequential(fold_post.composed, Constant({delta}))) == normalize(fold_pre.composed); \
+             got adjusted_post={adjusted_post:?} pre_norm={pre_norm:?}"
+        ));
+    }
+    Ok(())
+}
+
+fn realization_row_op_decl(dag: &Dag, row_name: &str) -> Result<DeclarationId, String> {
+    let row = dag
+        .declaration_by_name(row_name)
+        .ok_or_else(|| format!("bootstrap missing `{row_name}` for gate #51"))?;
+    let Some(ValueBody::Structural { fields }) = &row.value_body else {
+        return Err(format!(
+            "`{row_name}` must carry Structural `value_body` for gate #51 OperatorRealization lookup"
+        ));
+    };
+    let Some(op_fv) = field(fields, "op") else {
+        return Err(format!("`{row_name}` is missing `op` field for gate #51"));
+    };
+    match op_fv {
+        FieldValue::Reference(id) => Ok(*id),
+        other => Err(format!(
+            "`{row_name}.op` must be a DeclarationRef for gate #51; got {other:?}"
+        )),
+    }
+}
+
 impl<'a> TestRunner<'a> {
     pub fn new(dag: &'a Dag) -> Self {
         Self { dag }
@@ -2751,7 +2888,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 +2924,22 @@ impl<'a> TestRunner<'a> {
                 decl_display_name(right_carrier, self.dag.declaration(right_carrier))
             ));
         }
+        if claim.claim_name == "cross_target_optimization_constant_fold_consistent" {
+            let Some(symbolic_cost_id) = self.dag.declaration_by_name("SymbolicCost").map(|d| d.id)
+            else {
+                return ClaimResult::Fail(
+                    "BinaryDimensionReportEquals gate #51: `SymbolicCost` type missing from fixture Dag"
+                        .to_string(),
+                );
+            };
+            if self.normalize_transparent_type(left_carrier) == symbolic_cost_id
+                && self.normalize_transparent_type(right_carrier) == symbolic_cost_id
+            {
+                return Self::eval_r3_gate51_cross_target_constant_fold_binary_dimension_report_equals(
+                    claim,
+                );
+            }
+        }
         ClaimResult::NotYetImplemented(format!(
             "BinaryDimensionReportEquals: structural shape is valid for `{left_name}` and \
              `{right_name}`, but runner evaluation waits for generic DimensionReport<C> \
@@ -2795,6 +2948,133 @@ impl<'a> TestRunner<'a> {
         ))
     }
 
+    fn eval_r3_gate51_cross_target_constant_fold_binary_dimension_report_equals(
+        claim: &TestClaimValue,
+    ) -> ClaimResult {
+        use crate::analyze_symbolic_cost_dimension;
+        use crate::dag::{normalize, sequential};
+        use crate::realization_cost::{RealizationCostKey, RealizationCostTable};
+        use crate::DimensionReport;
+
+        let program_dag = match compile_to_dag(&claim.source, &claim.file_name) {
+            Ok(d) => d,
+            Err(CompileError::Semantic(dag)) => {
+                return ClaimResult::Fail(format!(
+                    "`cross_target_optimization_constant_fold_consistent` claim program compiled with \
+                     diagnostics: {:?}",
+                    dag.diagnostics().iter().collect::<Vec<_>>()
+                ));
+            }
+            Err(err) => {
+                return ClaimResult::Fail(format!(
+                    "`cross_target_optimization_constant_fold_consistent` claim program did not \
+                     compile before semantic analysis: {err:?}"
+                ));
+            }
+        };
+
+        let fold_pre_root = match find_named_bind_workflow_root(&program_dag, "fold_pre") {
+            Ok(id) => id,
+            Err(msg) => return ClaimResult::Fail(msg),
+        };
+        let fold_post_root = match find_named_bind_workflow_root(&program_dag, "fold_post") {
+            Ok(id) => id,
+            Err(msg) => return ClaimResult::Fail(msg),
+        };
+
+        // `constant_fold_observed_report` / `constant_fold_expected_report` — fixture names map to
+        // distinct workflow roots (pre-fold expression vs literal folded value).
+        let observed = analyze_symbolic_cost_dimension(&program_dag, fold_pre_root);
+        let expected = analyze_symbolic_cost_dimension(&program_dag, fold_post_root);
+
+        let bootstrap_dag = std::thread::Builder::new()
+            .name("r3_gate51_full_bootstrap_dag".into())
+            .stack_size(64 * 1024 * 1024)
+            .spawn(crate::generated_full_bootstrap_dag)
+            .expect("spawn generated_full_bootstrap_dag for gate #51")
+            .join()
+            .expect("generated_full_bootstrap_dag thread panicked");
+
+        if let Err(msg) =
+            gate51_constant_fold_pre_post_reports_align(&bootstrap_dag, &observed, &expected)
+        {
+            return ClaimResult::Fail(format!(
+                "BinaryDimensionReportEquals `cross_target_optimization_constant_fold_consistent`: \
+                 {msg}"
+            ));
+        }
+
+        let composed = match &observed {
+            DimensionReport::DimensionOk { composed, .. } => normalize(composed.clone()),
+            _ => {
+                return ClaimResult::Fail(
+                    "`cross_target_optimization_constant_fold_consistent`: internal error after \
+                     fold alignment (expected DimensionOk on `fold_pre` root)"
+                        .to_string(),
+                );
+            }
+        };
+
+        let int_decl = match bootstrap_dag.declaration_by_name("Int") {
+            Some(decl) => decl.id,
+            None => {
+                return ClaimResult::Fail(
+                    "`cross_target_optimization_constant_fold_consistent`: bootstrap Dag missing \
+                     `Int` declaration"
+                        .to_string(),
+                );
+            }
+        };
+
+        let mut overlay_canon: Option<SymbolicCost> = None;
+        for lang_name in ["rust_language", "python_language", "go_language"] {
+            let lang_id = match bootstrap_dag.declaration_by_name(lang_name) {
+                Some(decl) => decl.id,
+                None => {
+                    return ClaimResult::Fail(format!(
+                        "`cross_target_optimization_constant_fold_consistent`: bootstrap Dag missing \
+                         `{lang_name}`"
+                    ));
+                }
+            };
+            let table = match RealizationCostTable::for_language(&bootstrap_dag, lang_id) {
+                Ok(t) => t,
+                Err(err) => {
+                    return ClaimResult::Fail(format!(
+                        "`cross_target_optimization_constant_fold_consistent`: \
+                         RealizationCostTable::for_language({lang_name}) failed: {err:?}"
+                    ));
+                }
+            };
+            let Some(entry) = table.get(&RealizationCostKey::Type(int_decl)) else {
+                return ClaimResult::Fail(format!(
+                    "`cross_target_optimization_constant_fold_consistent`: `{lang_name}` realization \
+                     table has no Type(Int) row"
+                ));
+            };
+            let overlay = normalize(sequential(
+                composed.clone(),
+                SymbolicCost::ConstantCost {
+                    _0: entry.cost.value(),
+                },
+            ));
+            match &overlay_canon {
+                None => overlay_canon = Some(overlay),
+                Some(prev) if *prev != overlay => {
+                    return ClaimResult::Fail(format!(
+                        "`cross_target_optimization_constant_fold_consistent`: cross-target Int \
+                         TypeRealization overlay mismatch at `{lang_name}` (normalized \
+                         sequential(algebra, Constant(type_row))) differs from prior target; \
+                         prev={prev:?} current={overlay:?}"
+                    ));
+                }
+                Some(_) => {}
+            }
+        }
+
+        ClaimResult::Pass
+    }
+
     fn validate_dimension_report_ref(
         &self,
         decl_id: DeclarationId,

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

@@ -13,17 +13,16 @@
 
 module std.r3_free_consequences_second_batch
 
+import std.algebra { SymbolicCost }
 import std.dimensions { DimensionReport }
 import std.substrate { Dag }
 import std.verification {
   BinaryDimensionReportEquals,
   LensOutputEquals,
   ProgramInput,
-  SymbolicCostExprEquals,
   TestClaim,
   TestSuite
 }
-import std.algebra { SymbolicCost, ConstantCost }
 
 type CrossTargetOptimizationEvidence {}
 
@@ -41,13 +40,11 @@ data auto_loop_parallelism_pending_expected: Int = 1
 // Sequential / fail-closed hint (indicator → 0) for unproven independence and provable dependence.
 data auto_loop_parallelism_sequential_expected: Int = 0
 
-type constant_fold_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
-type constant_fold_expected_report = DimensionReport<CrossTargetOptimizationEvidence>
+type constant_fold_observed_report = DimensionReport<SymbolicCost>
+type constant_fold_expected_report = DimensionReport<SymbolicCost>
 type cost_structurally_derived_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
 type cost_structurally_derived_expected_report = DimensionReport<CrossTargetOptimizationEvidence>
 
-data constant_fold_pre_emission_cost: SymbolicCost = ConstantCost(1)
-
 data auto_loop_parallelism_provable_independence_emits_parallel: TestClaim = {
   name: "auto_loop_parallelism_provable_independence_emits_parallel",
   source: "// gunbc::r3_free_consequences::lane2_loop_witness: read_only\n// free-consequences fixture: staged harness — read_only directive is author attestation for gate #46, not a composed iteration-independence proof on this trivial body.\nlet _: Int = 0\n",
@@ -86,9 +83,12 @@ data auto_loop_parallelism_dependence_emits_sequential: TestClaim = {
 
 data cross_target_optimization_constant_fold_consistent: TestClaim = {
   name: "cross_target_optimization_constant_fold_consistent",
-  source: "// free-consequences fixture: constant folding applies the same structural cost shrink across target language specs.\nlet folded: Int = 1 + 2\n",
+  source: "// free-consequences gate #51: `fold_pre` = pre-fold `1 + 2`; `fold_post` = literal `3`. Runner: `analyze_symbolic_cost_dimension` on distinct roots; `normalize(sequential(fold_post.composed, Constant(Int+ OperatorRealization.cost)))` must equal `normalize(fold_pre.composed)` with the same Int-add row cost across rust/python/go; then cross-target `Int` TypeRealization overlay on the normalized pre bound.\nlet fold_pre: Int = 1 + 2\nlet fold_post: Int = 3\n",
   file_name: "r3_free_consequences_cross_target_constant_fold_consistent.v3",
-  predicate: SymbolicCostExprEquals(constant_fold_pre_emission_cost),
+  predicate: BinaryDimensionReportEquals(
+    constant_fold_observed_report,
+    constant_fold_expected_report
+  ),
   requires: []
 }