From 311bdee07e20d655f9b3cf46e371ffa14ae1ada4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 12:50:03 -0400 Subject: [PATCH 1/3] WIP: R3 gate #37: cost_lens_reads_target_realization (T-CostLens-Composition) --- src/v3/compiler/src/lib.rs | 16 ++++++- .../lens_cost_target_realization_test.rs | 47 ++++++++++--------- .../r3_free_consequences_second_batch_test.rs | 17 ++++--- 3 files changed, 50 insertions(+), 30 deletions(-) diff --git a/src/v3/compiler/src/lib.rs b/src/v3/compiler/src/lib.rs index 29dcfa7670d..21485ed8685 100644 --- a/src/v3/compiler/src/lib.rs +++ b/src/v3/compiler/src/lib.rs @@ -65,7 +65,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 @@ -259,6 +262,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, + ) -> SymbolicCost { + costs.into_iter().fold(algebra_cost, |acc, cost| { + sequential(acc, SymbolicCost::ConstantCost { _0: cost.value() }) + }) + } + struct RealizationMetas { type_meta: DeclarationId, callable_meta: DeclarationId, diff --git a/src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs b/src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs index 0afd9e7576a..be31a8ea81e 100644 --- a/src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs +++ b/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:?}" 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 15e31cee52d..f8b985bec91 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 @@ -20,13 +20,16 @@ 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_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; @@ -180,6 +183,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::>(); assert_eq!( realized_costs, @@ -250,7 +254,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]) }) } @@ -272,7 +276,7 @@ fn realization_cost( table: &RealizationCostTable, int_decl: DeclarationId, op: DeclarationId, -) -> i64 { +) -> RealizationCostAmount { table .cost(&RealizationCostKey::Operator { target: int_decl, @@ -281,7 +285,6 @@ fn realization_cost( .unwrap_or_else(|| { panic!("missing Rust LanguageSpec realization cost for operator row {op:?}") }) - .value() } fn compose_observed_structural_cost( @@ -293,7 +296,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]) }) } From 5e689b00d4d05144404bd3c49004d8051d37257b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 18:03:01 +0000 Subject: [PATCH 2/3] docs: add gate 37 hand-rust receipt --- 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 0c60aaa28e2..5a748d130e2 100644 --- a/docs/r3-program-plan.md +++ b/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::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::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 hand-Rust receipt (PR #3086):** `v3_compiler::realization_cost::compose_symbolic_cost_with_realization_costs` is a narrow Rust-side consumer wrapper over the existing `Semiring::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` `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 | **INTEGRATION_RECEIPT** — `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`). | `TestRunner` structural `SymbolicCost` comparison + representative program | From 397ffbc844d744462df9b6f60be37de25025c54a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 14 May 2026 20:24:16 +0000 Subject: [PATCH 3/3] docs: make gate 37 P5 receipt checkable --- 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 6fb8b6b0108..62245a2c152 100644 --- a/docs/r3-program-plan.md +++ b/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::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 hand-Rust receipt (PR #3086):** `v3_compiler::realization_cost::compose_symbolic_cost_with_realization_costs` is a narrow Rust-side consumer wrapper over the existing `Semiring::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 | +| 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::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::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` `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 |