R3 gate #37: cost_lens_reads_target_realization (T-CostLens-Composition)

docs/r3-program-plan.md

@@ -261,7 +261,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 34 | `bridge_include_str_side_channels_retired` | state-check | T-Bridge-Retirement | **CONSUMER_LANDED (slice scope)** (PR #2459 squash 2026-05-10 00:05Z — `pipeline.dag` compile-time embed slice retired with structural `PipelineStageBinding` bootstrap witness + `l1_5_fixed_point_test.rs` reintroduction ratchet per `src/v3/std/bridge_ledger.dag` header) | slice-scope; **standalone closure brief #1976 STOP-BLOCKED** on Substrate T1 (compile-body witness) per `pipeline_authority.rs` `fn compile` still `ArrowBody::Unparsed` (#1939 substrate dep, clever-cat-146 verification 2026-05-09) |
 | 35 | `bridge_exact_string_patching_residual_retired` | state-check | T-Bridge-Retirement | **PASSING** | PB lower-helper slice retired in `bridge_ledger.dag`; residual Row-4 classes → `bridge_exact_string_semantic_patching_residual` (Open) |
 | 36 | `bridge_retirement_ledger_zero` | ledger-count | T-Bridge-Retirement | DECLARED | unified ledger reports 0 |
-| 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — `src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs` pins `cost_lens_composes_symbolic_cost_with_rust_type_realization_row` (Rust-side `symbolic_cost_of` × `Semiring<SymbolicCost>::sequential` × bootstrap `rust_int.TypeRealization.cost`) and `cost_lens_reads_cost_field_on_rust_callable_realization_row` (`rust_is_empty_callable.CallableRealization.cost`). ε ratification (Q-Cost-Composition-Layering / PR #2181): lens output stays abstract `SymbolicCost`; per-primitive realization rows remain emit-time facts — **gates #40 + #70** now carry separate integration receipts in `m1_5_verification_test.rs` + the same `lens_cost_target_realization_test.rs` module (2026-05-12 bundle); row #37 remains the partial ε-slice for composition-row wiring alone. | Rust-side composition consumer + cited integration tests |
+| 37 | `cost_lens_reads_target_realization` | structural-fold | T-CostLens-Composition | **INTEGRATION_RECEIPT (partial — ε-slice)** — `src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs` pins `cost_lens_composes_symbolic_cost_with_rust_type_realization_row` (Rust-side `symbolic_cost_of` × `Semiring<SymbolicCost>::sequential` × bootstrap `rust_int.TypeRealization.cost`) and `cost_lens_reads_cost_field_on_rust_callable_realization_row` (`rust_is_empty_callable.CallableRealization.cost`). ε ratification (Q-Cost-Composition-Layering / PR #2181): lens output stays abstract `SymbolicCost`; per-primitive realization rows remain emit-time facts — **gates #40 + #70** now carry separate integration receipts in `m1_5_verification_test.rs` + the same `lens_cost_target_realization_test.rs` module (2026-05-12 bundle); row #37 remains the partial ε-slice for composition-row wiring alone. **P5 Mechanism (b) deferral receipt (PR #3086):** expanded non-test hand-Rust in existing SG-0 path `src/v3/compiler/src/lib.rs`; lane **T-PB-A**; concrete row **`ROADMAP.md` § "Lane acceptance — .dag gates" / `pb_hand_rust_at_shim_floor`** (the file remains under the SG-0 non-test census until PB-zero / pipeline-emitted Rust dissolves hand-maintained compiler helpers). Supporting single-authority evidence: `v3_compiler::realization_cost::compose_symbolic_cost_with_realization_costs` is a narrow Rust-side consumer wrapper over the existing `Semiring<SymbolicCost>::sequential` + `ConstantCost` composition, takes only validated `RealizationCostAmount` values from `RealizationCostTable`, and is exercised by `lens_cost_target_realization_test.rs` plus `r3_free_consequences_second_batch_test.rs`; it introduces no second realization-cost authority. | Rust-side composition consumer + cited integration tests |
 | 38 | `coercion_cost_equals_complexity_by_construction` | structural-fold | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `Semiring<SymbolicCost>` `sequential`/`iterate` at `src/v3/std/algebra.dag:181-188` is sole composition authority — no parallel "complexity-vs-cost" reconciliation surface exists) | thesis unification holds structurally |
 | 39 | `no_coercion_cost_dimension` | substrate-shape | T-CostLens-Composition | **SATISFIED-BY-CONSTRUCTION** (α-narrow PR #2171; `SymbolicCost` 7-variant at `src/v3/std/algebra.dag:181` is the sole cost dimension; no parallel `CoercionCost` carrier exists at HEAD per grep) | no separate cost dimension |
 | 40 | `symbolic_cost_expr_equals_executable` | SymbolicCost-typed | T-CostLens-Composition | **CONSUMER_LANDED + PASSING** — `m1_5_verification_test.rs`: `symbolic_cost_expr_equals_smoke_suite_passes` (literal `ConstantCost` path) + `symbolic_cost_expr_equals_countdown_demo_suite_passes` (independent `countdown` linear-semantics pin via `assert_recursive_countdown_linear_semantics`, then representative-program **executability + v3 literal roundtrip** for `demo`: `symbolic_cost_of` → `symbolic_cost_verification_fixture` → `SymbolicCostExprEquals` / `TestRunner`); `symbolic_cost_expr_equals_fail_closed_*` pins type + value mismatch fail-closed paths on `ClaimResult::Fail` (not `NotYetImplemented`). NYI-shell-retirement invariant pinned behavior-first by `symbolic_cost_expr_equals_executable_ratchet_test.rs` — single `TestRunner::run_suite` test (`symbolic_cost_expr_equals_well_shaped_claim_passes_and_never_returns_not_yet_implemented`) asserts `ClaimResult::Pass` and forbids both `NotYetImplemented(_)` (dispatch-fallthrough) and `Fail(_)` (evaluator regression) on the well-shaped path; fail-closed dispatch-arm tripwire, robust to dispatch reshaping / helper renames / message-text edits. Typed-shape rejection / fail-closed Fail-path coverage lives in `m1_5_verification_test.rs::symbolic_cost_expr_equals_fail_closed_*` (not duplicated in the ratchet file). | `TestRunner` structural `SymbolicCost` comparison + representative program |

src/v3/compiler/src/lib.rs

@@ -66,7 +66,10 @@ pub mod realization_cost {
 
     use std::collections::HashMap;
 
-    use crate::dag::{literal_decimal_i64, Dag, DeclarationId, FieldValue, LiteralBits, ValueBody};
+    use crate::dag::{
+        literal_decimal_i64, sequential, Dag, DeclarationId, FieldValue, LiteralBits, SymbolicCost,
+        ValueBody,
+    };
 
     /// 🟢 GREEN (terminal): closed mirror of the six `*Realization`
     /// meta-types in `src/v3/std/emit_model.dag`; each variant selects a
@@ -260,6 +263,17 @@ pub mod realization_cost {
         }
     }
 
+    /// Compose the target-agnostic symbolic cost with target realization
+    /// costs read from a `LanguageSpec` row table.
+    pub fn compose_symbolic_cost_with_realization_costs(
+        algebra_cost: SymbolicCost,
+        costs: impl IntoIterator<Item = RealizationCostAmount>,
+    ) -> SymbolicCost {
+        costs.into_iter().fold(algebra_cost, |acc, cost| {
+            sequential(acc, SymbolicCost::ConstantCost { _0: cost.value() })
+        })
+    }
+
     struct RealizationMetas {
         type_meta: DeclarationId,
         callable_meta: DeclarationId,

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

@@ -16,9 +16,9 @@
 
 use v3_compiler::compile_to_dag;
 use v3_compiler::dag::{
-    literal_decimal_i64, per_call_descent_evidence, sequential, ArithmeticOp, Behavior,
-    ComparisonOp, Dag, Declaration, DeclarationId, FieldValue, LiteralBits, OperatorKind,
-    SymbolicCost, TransformTarget, ValueBody,
+    literal_decimal_i64, per_call_descent_evidence, ArithmeticOp, Behavior, ComparisonOp, Dag,
+    Declaration, DeclarationId, FieldValue, LiteralBits, OperatorKind, SymbolicCost,
+    TransformTarget, ValueBody,
 };
 use v3_compiler::emit_rust::emit_rust;
 use v3_compiler::generated_full_bootstrap_dag;
@@ -28,7 +28,8 @@ use v3_compiler::lens_cost_target_realization::{
     pattern_realization_meta, type_instantiation_realization_meta, type_realization_meta,
 };
 use v3_compiler::realization_cost::{
-    RealizationCostCategory, RealizationCostKey, RealizationCostTable,
+    compose_symbolic_cost_with_realization_costs, RealizationCostCategory, RealizationCostKey,
+    RealizationCostTable,
 };
 
 use crate::common::assert_recursive_countdown_linear_semantics;
@@ -187,11 +188,13 @@ fn cost_lens_composes_symbolic_cost_with_rust_type_realization_row() {
             "literal bind should stay constant zero at algebra layer, got {algebra_cost:?}"
         );
 
-        let composed = sequential(
+        let table = RealizationCostTable::for_language(&boot, named_id(&boot, "rust_language"))
+            .expect("rust realization-cost table should build");
+        let composed = compose_symbolic_cost_with_realization_costs(
             algebra_cost,
-            SymbolicCost::ConstantCost {
-                _0: target_primitive_cost,
-            },
+            [table
+                .cost(&RealizationCostKey::Type(named_id(&boot, "Int")))
+                .expect("Rust Int realization cost")],
         );
         assert!(
             matches!(composed, SymbolicCost::ConstantCost { _0: 1 }),
@@ -368,40 +371,40 @@ let demo: Int = countdown(3) + 1
 
         let type_cost = table
             .cost(&RealizationCostKey::Type(int_decl))
-            .expect("Rust Int realization cost")
-            .value();
+            .expect("Rust Int realization cost");
         let add_cost = table
             .cost(&RealizationCostKey::Operator {
                 target: int_decl,
                 op: add_op,
             })
-            .expect("Rust Int add realization cost")
-            .value();
+            .expect("Rust Int add realization cost");
         let sub_cost = table
             .cost(&RealizationCostKey::Operator {
                 target: int_decl,
                 op: sub_op,
             })
-            .expect("Rust Int sub realization cost")
-            .value();
+            .expect("Rust Int sub realization cost");
         let eq_cost = table
             .cost(&RealizationCostKey::Operator {
                 target: int_decl,
                 op: eq_op,
             })
-            .expect("Rust Int eq realization cost")
-            .value();
+            .expect("Rust Int eq realization cost");
         assert_eq!(
-            (type_cost, add_cost, sub_cost, eq_cost),
+            (
+                type_cost.value(),
+                add_cost.value(),
+                sub_cost.value(),
+                eq_cost.value()
+            ),
             (1, 1, 1, 1),
             "fixture rows should expose Rust Int/Add/Sub/Eq realization costs"
         );
 
-        let composed = [type_cost, add_cost, sub_cost, eq_cost]
-            .into_iter()
-            .fold(algebra_cost, |acc, cost| {
-                sequential(acc, SymbolicCost::ConstantCost { _0: cost })
-            });
+        let composed = compose_symbolic_cost_with_realization_costs(
+            algebra_cost,
+            [type_cost, add_cost, sub_cost, eq_cost],
+        );
         assert!(
             mentions_linear(&composed),
             "cost lens demo should preserve the observable linear bound while folding Rust realization rows, got {composed:?}"

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

@@ -24,14 +24,17 @@ use std::sync::OnceLock;
 
 use v3_compiler::compile_to_dag;
 use v3_compiler::dag::{
-    sequential, ArithmeticOp, Behavior, ComparisonOp, Dag, DeclarationId, OperatorKind,
-    SymbolicCost, TransformTarget,
+    ArithmeticOp, Behavior, ComparisonOp, Dag, DeclarationId, OperatorKind, SymbolicCost,
+    TransformTarget,
 };
 use v3_compiler::emit_rust::emit_rust;
 use v3_compiler::generated_full_bootstrap_dag;
 use v3_compiler::lens_cost::{complexity_of, ComplexityLookup};
 use v3_compiler::lens_cost_symbolic::{symbolic_cost_of, SymbolicCostLookup};
-use v3_compiler::realization_cost::{RealizationCostKey, RealizationCostTable};
+use v3_compiler::realization_cost::{
+    compose_symbolic_cost_with_realization_costs, RealizationCostAmount, RealizationCostKey,
+    RealizationCostTable,
+};
 use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner};
 use v3_compiler::CompileError;
 
@@ -188,6 +191,7 @@ let demo: Int = countdown(3) + 1
     let realized_costs = realized_rows
         .iter()
         .map(|row| realization_cost(&table, int_decl, row.op))
+        .map(|cost| cost.value())
         .collect::<Vec<_>>();
     assert_eq!(
         realized_costs,
@@ -284,7 +288,7 @@ fn compose_expected_structural_cost(
     rows.into_iter()
         .map(|row| realization_cost(table, int_decl, row.op))
         .fold(algebra_cost, |acc, primitive_cost| {
-            sequential(acc, SymbolicCost::ConstantCost { _0: primitive_cost })
+            compose_symbolic_cost_with_realization_costs(acc, [primitive_cost])
         })
 }
 
@@ -306,7 +310,7 @@ fn realization_cost(
     table: &RealizationCostTable,
     int_decl: DeclarationId,
     op: DeclarationId,
-) -> i64 {
+) -> RealizationCostAmount {
     table
         .cost(&RealizationCostKey::Operator {
             target: int_decl,
@@ -315,7 +319,6 @@ fn realization_cost(
         .unwrap_or_else(|| {
             panic!("missing Rust LanguageSpec realization cost for operator row {op:?}")
         })
-        .value()
 }
 
 fn compose_observed_structural_cost(
@@ -327,7 +330,7 @@ fn compose_observed_structural_cost(
     rows.iter()
         .map(|row| realization_cost(table, int_decl, row.op))
         .fold(algebra_cost, |acc, primitive_cost| {
-            sequential(acc, SymbolicCost::ConstantCost { _0: primitive_cost })
+            compose_symbolic_cost_with_realization_costs(acc, [primitive_cost])
         })
 }