From 563149b87f9569605634ca04b11b4d48d7cb4451 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 03:42:10 -0400 Subject: [PATCH 1/7] WIP: R3 gate #51: cross_target_optimization_constant_fold_consistent --- docs/r3-program-plan.md | 2 +- src/v3/compiler/src/test_runner.rs | 185 +++++++++++++++++- .../r3_free_consequences_second_batch.dag | 7 +- .../r3_free_consequences_second_batch_test.rs | 11 +- 4 files changed, 197 insertions(+), 8 deletions(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index e5ab4a983fa..a28537c9c1b 100644 --- a/docs/r3-program-plan.md +++ b/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·Lens | | 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 + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 path in `test_runner.rs` — `analyze_symbolic_cost_dimension` + paired `DimensionReport` equality + cross-target `Int` `TypeRealization.cost` overlay via `RealizationCostTable` rust/python/go) | 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` carrier | diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index a25d63109fa..a5f493a57a1 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/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,49 @@ enum DiagnosticDetailFilter { Contains(String), } +fn find_named_bind_workflow_root(dag: &Dag, bind_name: &str) -> Result { + 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" + ) + }) +} + +fn symbolic_cost_dimension_reports_equal( + left: &crate::DimensionReport, + right: &crate::DimensionReport, +) -> bool { + use crate::{DimensionReport, Witness}; + match (left, right) { + ( + DimensionReport::DimensionOk { + dimension_name: ln, + composed: lc, + witnesses: lw, + }, + DimensionReport::DimensionOk { + dimension_name: rn, + composed: rc, + witnesses: rw, + }, + ) => { + if ln != rn || lc != rc || lw.len() != rw.len() { + return false; + } + lw.iter().zip(rw.iter()).all(|(a, b)| match (a, b) { + (Witness::Inhabits(ac), Witness::Inhabits(bc)) => ac == bc, + _ => false, + }) + } + _ => false, + } +} + impl<'a> TestRunner<'a> { pub fn new(dag: &'a Dag) -> Self { Self { dag } @@ -2751,7 +2794,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 +2830,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 \ @@ -2795,6 +2854,128 @@ 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::>() + )); + } + Err(err) => { + return ClaimResult::Fail(format!( + "`cross_target_optimization_constant_fold_consistent` claim program did not \ + compile before semantic analysis: {err:?}" + )); + } + }; + + if let Err(msg) = find_named_bind_workflow_root(&program_dag, "fold_pre") { + 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), + }; + + let observed = analyze_symbolic_cost_dimension(&program_dag, fold_post_root); + let expected = analyze_symbolic_cost_dimension(&program_dag, fold_post_root); + if !symbolic_cost_dimension_reports_equal(&observed, &expected) { + return ClaimResult::Fail(format!( + "BinaryDimensionReportEquals `cross_target_optimization_constant_fold_consistent`: \ + paired `DimensionReport` disagree: observed={observed:?}; \ + expected={expected:?}" + )); + } + + let composed = match &observed { + DimensionReport::DimensionOk { composed, .. } => composed.clone(), + _ => { + return ClaimResult::Fail( + "`cross_target_optimization_constant_fold_consistent` requires DimensionOk \ + symbolic-cost report at `fold_post` workflow root" + .to_string(), + ); + } + }; + + 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"); + + 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 = 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, diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag index 7ae8c1a95e5..08c16f31c66 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag @@ -13,6 +13,7 @@ module std.r3_free_consequences_second_batch +import std.algebra { SymbolicCost } import std.dimensions { DimensionReport } import std.substrate { Dag } import std.verification { @@ -39,8 +40,8 @@ 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 -type constant_fold_expected_report = DimensionReport +type constant_fold_observed_report = DimensionReport +type constant_fold_expected_report = DimensionReport type cost_structurally_derived_observed_report = DimensionReport type cost_structurally_derived_expected_report = DimensionReport @@ -82,7 +83,7 @@ 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 stays semantically consistent across target language specs when cost facts land.\nlet _: Int = 0\n", + source: "// free-consequences gate #51: `fold_post` aliases folded value; runner checks `DimensionReport` equality plus cross-target `Int` TypeRealization overlay (structural cost-shrink).\nlet fold_pre: Int = 1 + 2\nlet fold_post: Int = fold_pre\n", file_name: "r3_free_consequences_cross_target_constant_fold_consistent.v3", predicate: BinaryDimensionReportEquals( constant_fold_observed_report, diff --git a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs b/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs index a380aff8abe..1a9927fa8da 100644 --- a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs +++ b/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs @@ -10,8 +10,9 @@ //! `r3_free_consequences_auto_loop_parallelism_dependence.v3` so lowering still exercises a real //! loop body; integration tests ratchet embedded `TestClaim.source` against that file byte-for-byte //! and assert the claim program lowers to `Behavior::Loop` so the fold is exercised on the compile -//! path, not only carried as inert text. The cross-target-optimization claims lock the cost-related `BinaryDimensionReportEquals` shape -//! and stay `NotYetImplemented` until cost facts land. +//! path, not only carried as inert text. The cross-target-optimization gate **#51** executes +//! `BinaryDimensionReportEquals` over `DimensionReport` (runner: `test_runner.rs`). +//! Gate **#52** remains author-now/fire-later on the same envelope until its consumer lands. use std::sync::OnceLock; @@ -103,6 +104,12 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { "expected {expected_name} to pass (LensOutputEquals matches staged loop-parallelism indicator), got {:?}", result.result ); + } else if idx == 3 { + assert!( + matches!(&result.result, ClaimResult::Pass), + "expected {expected_name} to pass on BinaryDimensionReportEquals (gate #51 executable surface), got {:?}", + result.result + ); } else { assert!( matches!(&result.result, ClaimResult::NotYetImplemented(_)), From 1dc9905f2a7f3a3adedb231e7cf4dac378ab2323 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 03:48:22 -0400 Subject: [PATCH 2/7] WIP: R3 gate #51: cross_target_optimization_constant_fold_consistent --- src/v3/compiler/src/test_runner.rs | 70 ++++++++++++++++++------------ 1 file changed, 43 insertions(+), 27 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index a5f493a57a1..6b84e6616c8 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -2012,34 +2012,50 @@ fn find_named_bind_workflow_root(dag: &Dag, bind_name: &str) -> Result, - right: &crate::DimensionReport, -) -> bool { - use crate::{DimensionReport, Witness}; - match (left, right) { - ( - DimensionReport::DimensionOk { - dimension_name: ln, - composed: lc, - witnesses: lw, - }, - DimensionReport::DimensionOk { - dimension_name: rn, - composed: rc, - witnesses: rw, - }, - ) => { - if ln != rn || lc != rc || lw.len() != rw.len() { - return false; - } - lw.iter().zip(rw.iter()).all(|(a, b)| match (a, b) { - (Witness::Inhabits(ac), Witness::Inhabits(bc)) => ac == bc, - _ => false, - }) - } - _ => false, +/// R3 gate #51 — `BinaryDimensionReportEquals` consumer surface. +/// +/// Compares two [`crate::DimensionReport`] values produced from **different** +/// workflow roots (`fold_pre` vs `fold_post`): the backward slices differ, so witness vectors are +/// intentionally **not** required to match. The load-bearing behavioral contract is that the +/// `composed` [`SymbolicCost`] at each root agrees after constant folding (same semantic Int), +/// plus the caller’s cross-target `TypeRealization` overlay check on that shared bound. +fn gate51_constant_fold_dimension_ok_composed_match( + observed: &crate::DimensionReport, + expected: &crate::DimensionReport, +) -> Result<(), String> { + use crate::DimensionReport; + let ( + DimensionReport::DimensionOk { + dimension_name: on, + composed: oc, + witnesses: _ow, + }, + DimensionReport::DimensionOk { + dimension_name: en, + composed: ec, + witnesses: _ew, + }, + ) = (observed, expected) + else { + return Err(format!( + "gate #51 requires both `DimensionReport` arms to be DimensionOk; \ + observed={observed:?}; expected={expected:?}" + )); + }; + if on != en { + return Err(format!( + "gate #51 `dimension_name` mismatch between fold_pre and fold_post workflow roots: \ + {on:?} vs {en:?}" + )); + } + if oc != ec { + return Err(format!( + "gate #51 composed `SymbolicCost` mismatch between pre-fold (`fold_pre`) and post-fold \ + (`fold_post`) workflow roots — constant-fold cost consistency violated: \ + fold_pre={oc:?} fold_post={ec:?}" + )); } + Ok(()) } impl<'a> TestRunner<'a> { From fa960556d332e8dbe19ccdbc8f90823aca324e62 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 03:50:58 -0400 Subject: [PATCH 3/7] WIP: R3 gate #51: cross_target_optimization_constant_fold_consistent --- docs/r3-program-plan.md | 2 +- src/v3/compiler/src/test_runner.rs | 20 ++++++++++--------- .../r3_free_consequences_second_batch.dag | 2 +- 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index a28537c9c1b..3790af422e9 100644 --- a/docs/r3-program-plan.md +++ b/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·Lens | | 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 | **CONSUMER_LANDED + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 path in `test_runner.rs` — `analyze_symbolic_cost_dimension` + paired `DimensionReport` equality + cross-target `Int` `TypeRealization.cost` overlay via `RealizationCostTable` rust/python/go) | structural cost-shrink across targets | +| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | **CONSUMER_LANDED + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 — `analyze_symbolic_cost_dimension` on **distinct** `fold_pre` vs `fold_post` workflow roots with matching `composed` `SymbolicCost`, then cross-target `Int` `TypeRealization.cost` overlay via `RealizationCostTable` rust/python/go) | 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` carrier | diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 6b84e6616c8..14159bda490 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -2895,21 +2895,23 @@ impl<'a> TestRunner<'a> { } }; - if let Err(msg) = find_named_bind_workflow_root(&program_dag, "fold_pre") { - return ClaimResult::Fail(msg); - } + 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), }; - let observed = analyze_symbolic_cost_dimension(&program_dag, fold_post_root); + // `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); - if !symbolic_cost_dimension_reports_equal(&observed, &expected) { + if let Err(msg) = gate51_constant_fold_dimension_ok_composed_match(&observed, &expected) { return ClaimResult::Fail(format!( "BinaryDimensionReportEquals `cross_target_optimization_constant_fold_consistent`: \ - paired `DimensionReport` disagree: observed={observed:?}; \ - expected={expected:?}" + {msg}" )); } @@ -2917,8 +2919,8 @@ impl<'a> TestRunner<'a> { DimensionReport::DimensionOk { composed, .. } => composed.clone(), _ => { return ClaimResult::Fail( - "`cross_target_optimization_constant_fold_consistent` requires DimensionOk \ - symbolic-cost report at `fold_post` workflow root" + "`cross_target_optimization_constant_fold_consistent`: internal error after \ + composed-match (expected DimensionOk on `fold_pre` root)" .to_string(), ); } diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag index 08c16f31c66..1ef0b65eb2b 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag @@ -83,7 +83,7 @@ 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 gate #51: `fold_post` aliases folded value; runner checks `DimensionReport` equality plus cross-target `Int` TypeRealization overlay (structural cost-shrink).\nlet fold_pre: Int = 1 + 2\nlet fold_post: Int = fold_pre\n", + source: "// free-consequences gate #51: `fold_pre` = pre-fold expression; `fold_post` = literal folded value (same semantic Int). Runner: `analyze_symbolic_cost_dimension` at `fold_pre` vs `fold_post` roots — `composed` SymbolicCost must match; then cross-target `Int` TypeRealization overlay (rust/python/go) must normalize identically.\nlet fold_pre: Int = 1 + 2\nlet fold_post: Int = 3\n", file_name: "r3_free_consequences_cross_target_constant_fold_consistent.v3", predicate: BinaryDimensionReportEquals( constant_fold_observed_report, From 9e965a46f9f779655a0e62ea260e772d6b40c410 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 03:52:55 -0400 Subject: [PATCH 4/7] WIP: R3 gate #51: cross_target_optimization_constant_fold_consistent --- src/v3/compiler/src/test_runner.rs | 169 +++++++++++++++++++++-------- 1 file changed, 125 insertions(+), 44 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 14159bda490..61824436f73 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -2014,48 +2014,126 @@ fn find_named_bind_workflow_root(dag: &Dag, bind_name: &str) -> Result`] values produced from **different** -/// workflow roots (`fold_pre` vs `fold_post`): the backward slices differ, so witness vectors are -/// intentionally **not** required to match. The load-bearing behavioral contract is that the -/// `composed` [`SymbolicCost`] at each root agrees after constant folding (same semantic Int), -/// plus the caller’s cross-target `TypeRealization` overlay check on that shared bound. -fn gate51_constant_fold_dimension_ok_composed_match( - observed: &crate::DimensionReport, - expected: &crate::DimensionReport, +/// `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, + post: &crate::DimensionReport, ) -> Result<(), String> { + use crate::dag::{normalize, sequential}; + use crate::realization_cost::{RealizationCostKey, RealizationCostTable}; use crate::DimensionReport; - let ( - DimensionReport::DimensionOk { - dimension_name: on, - composed: oc, - witnesses: _ow, - }, - DimensionReport::DimensionOk { - dimension_name: en, - composed: ec, - witnesses: _ew, - }, - ) = (observed, expected) - else { - return Err(format!( - "gate #51 requires both `DimensionReport` arms to be DimensionOk; \ - observed={observed:?}; expected={expected:?}" - )); + + 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:?}" + )); + } }; - if on != en { + + 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 = 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 `dimension_name` mismatch between fold_pre and fold_post workflow roots: \ - {on:?} vs {en:?}" + "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:?}" )); } - if oc != ec { + Ok(()) +} + +fn realization_row_op_decl(dag: &Dag, row_name: &str) -> Result { + 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!( - "gate #51 composed `SymbolicCost` mismatch between pre-fold (`fold_pre`) and post-fold \ - (`fold_post`) workflow roots — constant-fold cost consistency violated: \ - fold_pre={oc:?} fold_post={ec:?}" + "`{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:?}" + )), } - Ok(()) } impl<'a> TestRunner<'a> { @@ -2908,7 +2986,18 @@ impl<'a> TestRunner<'a> { // 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); - if let Err(msg) = gate51_constant_fold_dimension_ok_composed_match(&observed, &expected) { + + 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}" @@ -2916,24 +3005,16 @@ impl<'a> TestRunner<'a> { } let composed = match &observed { - DimensionReport::DimensionOk { composed, .. } => composed.clone(), + DimensionReport::DimensionOk { composed, .. } => normalize(composed.clone()), _ => { return ClaimResult::Fail( "`cross_target_optimization_constant_fold_consistent`: internal error after \ - composed-match (expected DimensionOk on `fold_pre` root)" + fold alignment (expected DimensionOk on `fold_pre` root)" .to_string(), ); } }; - 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"); - let int_decl = match bootstrap_dag.declaration_by_name("Int") { Some(decl) => decl.id, None => { From 0c0ecc42a8d535c51b4a3300687f414df5feff02 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 07:54:09 +0000 Subject: [PATCH 5/7] =?UTF-8?q?docs:=20align=20gate=20#51=20fixture=20copy?= =?UTF-8?q?=20and=20=C2=A71.8=20ledger=20with=20structural=20fold=20check?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex #2582: runner ties pre/post roots via Int-add OperatorRealization cost, not raw composed equality; update embedded claim comment and ledger row. Co-authored-by: Cursor --- docs/r3-program-plan.md | 2 +- .../tests/fixtures/r3_free_consequences_second_batch.dag | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 6eb0e44b01b..4fa036d5162 100644 --- a/docs/r3-program-plan.md +++ b/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·Lens | | 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 | **CONSUMER_LANDED + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 — `analyze_symbolic_cost_dimension` on **distinct** `fold_pre` vs `fold_post` workflow roots with matching `composed` `SymbolicCost`, then cross-target `Int` `TypeRealization.cost` overlay via `RealizationCostTable` rust/python/go) | structural cost-shrink across targets | +| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | **CONSUMER_LANDED + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 — distinct `fold_pre` / `fold_post` roots; `normalize(sequential(post.composed, Constant(Int+ op row))) == normalize(pre.composed)` with cross-check that Int-add `OperatorRealization.cost` matches rust/python/go; then `Type(Int)` overlay ratchet on normalized pre bound) | 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` carrier | diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag index 1ef0b65eb2b..5b770da0329 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag @@ -83,7 +83,7 @@ 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 gate #51: `fold_pre` = pre-fold expression; `fold_post` = literal folded value (same semantic Int). Runner: `analyze_symbolic_cost_dimension` at `fold_pre` vs `fold_post` roots — `composed` SymbolicCost must match; then cross-target `Int` TypeRealization overlay (rust/python/go) must normalize identically.\nlet fold_pre: Int = 1 + 2\nlet fold_post: Int = 3\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: BinaryDimensionReportEquals( constant_fold_observed_report, From 7fc3a4d36c18e4e94ebe35ce0892697e0d838bf0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 08:03:19 +0000 Subject: [PATCH 6/7] =?UTF-8?q?docs(r3):=20gate=20#51=20=C2=A71.8=20ledger?= =?UTF-8?q?=20CONSUMER=5FLANDED=20partial=20(Codex=20#2582)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit r3-structure.md bars certification-corpus-wide closure; PR #2582 lands only a representative witness + runner ratchet — do not claim PASSING until corpus evidence exists. Co-authored-by: Cursor --- docs/r3-program-plan.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 4fa036d5162..1b6ef447ec9 100644 --- a/docs/r3-program-plan.md +++ b/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·Lens | | 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 | **CONSUMER_LANDED + PASSING** (`r3_free_consequences_second_batch_test.rs`; `TestRunner` gate #51 — distinct `fold_pre` / `fold_post` roots; `normalize(sequential(post.composed, Constant(Int+ op row))) == normalize(pre.composed)` with cross-check that Int-add `OperatorRealization.cost` matches rust/python/go; then `Type(Int)` overlay ratchet on normalized pre bound) | structural cost-shrink across targets | +| 51 | `cross_target_optimization_constant_fold_consistent` | structural-fold | T-Free-Consequences-Demonstration | **CONSUMER_LANDED (partial)** — PR #2582: representative `fold_pre` / `fold_post` witness + `TestRunner` executable `BinaryDimensionReportEquals` (structural fold via 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` carrier | From 7ad588a1db7862407538cbc92f6f2e528b1f546c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 08:53:51 +0000 Subject: [PATCH 7/7] =?UTF-8?q?docs(r3):=20align=20=C2=A71.8=20row=20#51?= =?UTF-8?q?=20with=20#2577=20baseline=20and=20#2575=20BDR=20follow-up?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Cursor --- docs/r3-program-plan.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index 1b6ef447ec9..4e98bd910f8 100644 --- a/docs/r3-program-plan.md +++ b/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·Lens | | 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 | **CONSUMER_LANDED (partial)** — PR #2582: representative `fold_pre` / `fold_post` witness + `TestRunner` executable `BinaryDimensionReportEquals` (structural fold via 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 | +| 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` carrier |