Wave-1 V3: #40 symbolic_cost_expr_equals + #70 cost_lens_demonstration bundle

INVARIANTS.md

@@ -334,6 +334,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX
 |------|---------|
 | `src/v3/compiler/tests/integration/anthropic_tool_result_wire_demo_test.rs` | **ROADMAP:** `ROADMAP.md` § **PR #901 (merged)** — third bullet (`anthropic_tool_result_full_content_surface`, PR #2711 nested tool-result wire) **and** § **LLM service flattening** (`rest_request_wire_serde_alignment`, nested Anthropic tool-result contracts). **Dissolution:** remove this file when Messages tool-result nested serde is emitted **only** from `dsl/extdeps/llm/anthropic.dag` `CoproductWireContract` authorities (no hand-maintained `Serialize` mirror). **Interim ratchet:** `tool_result_wire_demo_projection_is_locked_to_modeled_dag_surface` pins demo field/variant shapes to `generated_full_bootstrap_dag()`. **Residual:** `structural_coverage_gap_anthropic_tool_result_nested_block_wire_payloads` in `dsl/extdeps/llm/anthropic.dag`. |
 | `src/v3/compiler/tests/integration/cementing/cost_lens_symbolic_consumer_test.rs` | **ROADMAP:** `ROADMAP.md` § **R3 gate #78 — unary-bind `SymbolicCost` iterate alias collapse post-pass** (`per_call_pattern_at` / host-wrapper alias-collapse residual, `e_p_sub_value_relation_per_call_landed`). **Dissolution:** remove this file when the cost-lens `symbolic_cost_of` host wrapper no longer owns the alias-collapse post-pass and the `per_call_pattern_at` unary-countdown assertion is carried by the modeled lens substrate / `.dag` receipt instead of hand Rust. **Interim ratchet:** `e_p_sub_value_relation_per_call_landed_cost_lens_routes_through_per_call_pattern_query` pins the remaining consumer to the shared substrate query. **Retired role:** gate #87 Band-C `cost_symbolic` COMPLETE cementing moved to `src/v3/compiler/tests/dag/t_r3_gate_87_cementing_regen_cost_symbolic.dag` and must not be counted against this hand-Rust receipt. |
+| `src/v3/compiler/tests/integration/common/symbolic_cost_verification_fixture.rs` | **ROADMAP:** `docs/r3-program-plan.md` §1.8 — T-CostLens-Composition gates **#40** (`symbolic_cost_expr_equals_executable`) + **#70** (`cost_lens_demonstration`) integration receipts (`m1_5_verification_test.rs` / `lens_cost_target_realization_test.rs`). **Dissolution:** remove when `TestClaim` fixtures can declare expected `SymbolicCost` values for dynamic `PortId`-anchored oracles without a host-side serializer (testgen or substrate-reflected literal emission aligned with `test_runner::field_value_to_symbolic_cost_eq_pattern`). **Interim ratchet:** `symbolic_cost_as_v3_data_initializer` + `escape_v3_string_literal_content` stay aligned with the runner’s structural decode rules; unit tests in-module pin `SumCost`/`LinearCost` surface spellings. |
 | `src/v3/compiler/tests/integration/cementing/cementing_provenance_origin_integration_test.rs` | **ROADMAP:** `ROADMAP.md` — Post-merge debt bullet **v3 lens capability honesty pass** (cementing-test discipline per `regen.dag`; see `docs/v3-lens-capability-register.md`). **Dissolution:** remove when `origin_of` provenance seam checks for gate-#87 regen harnesses live as `.dag` `TestClaim` obligations alongside `tests/dag/cementing_dispatch.dag` (no Rust mirror of the dispatch projection from `std.verification`'s `lens_capability_register_rows`). **Interim ratchet:** narrow slice split from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
 | `src/v3/compiler/tests/integration/common/wiring_scanner_test.rs` | **ROADMAP:** same **v3 lens capability honesty pass** bullet — Band-C `tests/integration.rs` `#[path]` wiring is enforced by `integration_rs_wiring_scan.rs` + `cementing_dispatch.rs`. **Dissolution:** remove when `integration.rs` wiring can be validated structurally for cementing modules without line scanners. **Interim ratchet:** unit tests for helpers promoted from the retired `cementing_lens_registry_dispatch_test.rs` monolith. |
 

docs/r3-program-plan.md

@@ -36,7 +36,7 @@ Each predicate has a passing TestClaim against representative input — **NOT**
 | TC2 (Church-Rosser) | `BinaryDimensionReportEquals` (DimensionReport-typed) | `tc2_church_rosser_executable` | T-V-L4-L7-Direct |
 | TC3 (Pattern-A second-mover) | `BinaryDimensionReportEquals` (DimensionReport-typed) | `tc3_pattern_a_second_mover_executable` | T-V-L4-L7-Direct |
 | RustDagIsomorphism | structural-equivalence assertion (Dag isomorphism, not DimensionReport) | `rust_dag_isomorphism_executable` | T-V-L4-L7-Direct |
-| SymbolicCostExprEquals | cost-predicate (`SymbolicCost`-typed; per `src/v3/compiler/src/test_runner.rs` `SymbolicCostExprEquals: structural shape is valid` NYI receipt) | `symbolic_cost_expr_equals_executable` | T-CostLens-Composition |
+| SymbolicCostExprEquals | cost-predicate (`SymbolicCost`-typed; `TestRunner` executes `SymbolicCostExprEquals` structurally via `SymbolicCostEqPattern` per `m1_5_verification_test.rs` gate **#40** receipts) | `symbolic_cost_expr_equals_executable` | T-CostLens-Composition |
 | BridgeLedgerZero | ledger-row count (Pattern E ratchet — decreasing-open-count, NOT DimensionReport; per `ROADMAP.md` §"Course correction #4" + `r3-structure.md` `bridge_retirement_ledger_zero` gate) | `bridge_retirement_ledger_zero` (existing) | T-Bridge-Retirement |
 | Free-Consequences-Demonstration | **composite of 10 gates** (NOT a single predicate; `r3-structure.md` §"Acceptance" → T-Free-Consequences-Demonstration gates) | (composite — see existing gates) | T-Free-Consequences-Demonstration |
 
@@ -260,10 +260,10 @@ 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 — full executable parity for gate **#40** / demonstration **#70** stays tracked separately. | 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. | 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 | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas); closes via Verification Mgr (#2075) ratchet authoring on Rust-side composition consumer + executable predicate per ε path | runtime prereq: cost lens consumer per ε |
+| 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` (representative recursive `countdown` + composed `demo` oracle serialized via `common/symbolic_cost_verification_fixture.rs`); `symbolic_cost_expr_equals_fail_closed_*` pins type + value mismatch fail-closed paths on `ClaimResult::Fail` (not `NotYetImplemented`). | `TestRunner` structural `SymbolicCost` comparison + representative program |
 | 41 | `v2_oracle_no_remaining_test_consumers` | state-check | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2695 squash 2026-05-11 — witty-crab-518 T-V2 G-1 ratchet: path/workspace/registry/TOML coverage + tc1 2s-ratchet exemption 79 rows; consumer-side check confirms no `.rs` test imports `src/v2/`) | no .rs test consumes src/v2/ |
 | 42 | `v2_directory_deleted` | state-check | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2693 squash 2026-05-11 — calm-seal-831 deleted entire `src/v2/` directory: -158,670 lines; row #97 `method_template_projection_emit_shim_retirement_coherence` fail-closed coherence test passes with v2/ absent, attesting G-2 guardrails per `docs/audit/t-v2-g2-deletion-plan-and-guardrails.md`) | src/v2/ removed from workspace |
 | 43 | `auto_parallelism_independent_binds_emit_parallel` | demonstration | T-Free-Consequences-Demonstration | **PASSING** (PR #2495 — parallel emit for independent binds landed 2026-05-10) | bind-independent → parallel emit |
@@ -293,7 +293,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
 | 67 | `numeric_construction_demonstration` | demonstration | T-Numeric-Construction | DECLARED (NEW 2026-05-06) | `Int<32>` + `Real<64>` round-trip |
 | 68 | `anthropic_wire_demonstration` | demonstration | T-Anthropic-Wire | **PASSING** (PR #2506 — codex anthropic wire demo merged 2026-05-10; `anthropic_messages_wire_demo_test.rs`) | deterministic mock; live-API NOT closure gate |
 | 69 | `bridge_retirement_demonstration` | demonstration | T-Bridge-Retirement | **PASSING** (PR #2551 — bridge retirement demonstration landed 2026-05-10) | integration `bridge_retirement_demonstration` (`canonical_lens_bridge_ratchet_test.rs`); typed-identity-surface executes through `LensOutputEquals` using fixture-local `DeclarationRef` resolution + production `apply_lens_declaration` |
-| 70 | `cost_lens_demonstration` | demonstration | T-CostLens-Composition | DECLARED — ε path RATIFIED 2026-05-07 (Q-Cost-Composition-Layering canvas at PR #2181); closes via Rust-side composition fixture demonstrating end-to-end cost reading per ε in T-CostLens follow-on slice | ≥2 algebra-instances + ≥1 recursive call |
+| 70 | `cost_lens_demonstration` | demonstration | T-CostLens-Composition | **INTEGRATION_RECEIPT** — `lens_cost_target_realization_test.rs::cost_lens_demonstration_composes_representative_rust_program_cost`: ≥2 algebra instances (Add/Sub/Eq) + recursive `countdown` call-site + `symbolic_cost_of` × `sequential` × `RealizationCostTable` composition; `common::assert_recursive_countdown_linear_semantics` on the abstract `countdown` carrier. | ≥2 algebra-instances + ≥1 recursive call |
 | 71 | `v3_self_host_demonstration` | demonstration | T-V2-Retirement | **CONSUMER_LANDED + PASSING** (PR #2696 squash `3e4bd97a` 2026-05-11 — still-crab-219 demonstration harness: fail-closed `--r3-gate-71-demonstration` path with in-memory `fixed_point_diff_ok` (C-5), `.dag` TestClaim + integration splice, SG-0 census + PR-body append, DB-8 strict flag, CI prepend + full-suite budget + TC1 slow-test exemption) | bootstrap PB-Runtime trampoline runs end-to-end |
 | 72 | `e_p_producer_demonstration` | demonstration | T-E-P-Producer-Broadening | **CONSUMER_LANDED** — integration `e_p_producer_demonstration` (`m2_substrate_inhabitance_test.rs`) | unary recursive self-call: `SubValueRelation` + scalar `per_call_pattern_at` → `lower_call_pattern` / `DescentEvidence::Strict` (multi-arg per-port vectors: other E-P tests) |
 | 73 | `lens_behavioral_parity_demonstration` | demonstration | T-Lens-Behavioral-Parity | DECLARED (NEW 2026-05-06) | **R3 (post-carve-promotion 2026-05-09):** all 4 lenses (complexity + cost + parallelism + effect_enum) vs frozen v2-oracle snapshot. Parallelism + effect_enum **R3-load-bearing within Cluster F** per Director carve-promotion ratification at gunbc#846 c#4412330468 (prior R4-carved status DISSOLVED). |
@@ -431,7 +431,7 @@ Each retires per its natural-owner program prerequisites. Verification Mgr's `br
 | T-Omni-Shape-B | YELLOW | **gate #25 salvage path active** at warm-dove-618 PB Mgr lane via assignment #2550 (after sleek-eagle-557 archival left PR #2410 orphan + DIRTY); **gate #26** (omni doc drift lock — snappy-heron-259) + **gate #27** (omni sql ddl alt — gentle-hawk-401) workers idle, mis-parented under sunny-koi-893 Grounding subtree pending re-parent coordination per gunbc#828 c#4414249641 | dependencies (R2-Evaluator landed; Shape A targets in flight) | post-gate-#25 salvage PR + #26/#27 closure |
 | T-Anthropic-Wire | YELLOW | 3 coproduct worker briefs dispatched on PR #1782 wait-window + 2 OPEN closure tags at HEAD (`dsl/extdeps/llm/anthropic.dag` `:189` + `:68`); **PR #2506 [codex] add anthropic wire demo MERGED 2026-05-10** (1 test entry: `anthropic_messages_wire_demo_test.rs`) | three coproduct slices land + variant-aware projection carrier authored | post-#1782 merge + 3 follow-up paydown PRs |
 | T-Bridge-Retirement | YELLOW | per-bridge dispatches. Cycle PR-merge evidence (gate-promotion separate; see Status column below): PR #2459 (`include_str` retire) + PR #2449 (`canonical lens name dispatch` retire) — both partial evidence toward §1.8 #34 / #33 promotion respectively. Per §1.8 canonical status: **#32 PASSING** (`mark_bootstrap_secret_nominal_opacity_retired`) + **#35 PASSING** (`bridge_exact_string_patching_residual_retired` — PB lower-helper slice retired in `bridge_ledger.dag`) + **#33 DECLARED** (canonical-lens-name dispatch; PR #2449 merged but gate not yet promoted) + **#34 DECLARED** (include_str side channels; PR #2459 merged but gate not yet promoted) | per §1.8: 2 retired-and-promoted (#32 + #35) + 2 retired-and-pending-promotion (#33 + #34) + remaining `SourceSpan.file participation` (Substrate-owned hand-Rust audit sites; not numbered in §1.8) + residual semantic patching (`bridge_exact_string_semantic_patching_residual` Open per #35 close-criterion). Aggregate retirement count per §1.8 PASSING discipline = 2/5 (gate-promotion-tied), with 2 awaiting promotion drift sweep | per `r3-structure.md` §"Lane structure" T-Bridge-Retirement R2-close-dependency: post-R2 substrate carriers + per-bridge gates per natural-owner program prerequisites |
-| T-CostLens-Composition | YELLOW | α-narrow ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 — gates **#38** + **#39** structurally satisfied at HEAD by construction (`SymbolicCost` sole cost dimension; `Semiring<SymbolicCost>` sole composition authority); receipts landed via PR #2171. **ε path RATIFIED 2026-05-07** (Q-Cost-Composition-Layering canvas at PR #2181, canonical-not-transitional) — **gate #37** documents the **partial** Rust-side composition consumer (`symbolic_cost` × `sequential` × bootstrap realization rows; see §1.8 row #37). **Gates #40** and **#70** remain **DECLARED** in §1.8 (Verification Mgr / follow-on slice + demonstration); full executable parity for #40 and closure for #70 are **not** claimed by #37’s ε-slice and stay **tracked separately** per row #37. **Q-Lens-Target-Context β-extended path DEFERRED** to N=2 trigger event (when second lens surfaces target-context need; emission_provenance most likely candidate per cross-cutting analysis); not active R3 ratification gate. | R2-Evaluator + R2-T-Substrate-Lens-Primitive + T-CostLens follow-on slice (Rust-side composition per ε) + Verification Mgr ratchet for #40 / demo closure for #70 | α close at HEAD; #37 partial ε-slice receipt only; #40 and #70 still open per §1.8 until their rows promote |
+| T-CostLens-Composition | YELLOW | α-narrow ratified at gunb-ai/gunbc#828 #issuecomment-4400772335 — gates **#38** + **#39** structurally satisfied at HEAD by construction (`SymbolicCost` sole cost dimension; `Semiring<SymbolicCost>` sole composition authority); receipts landed via PR #2171. **ε path RATIFIED 2026-05-07** (Q-Cost-Composition-Layering canvas at PR #2181, canonical-not-transitional) — **gate #37** documents the **partial** Rust-side composition consumer (`symbolic_cost` × `sequential` × bootstrap realization rows; see §1.8 row #37). **Gates #40** + **#70** carry **INTEGRATION_RECEIPT** evidence at §1.8 (2026-05-12 PR #2785: `m1_5_verification_test.rs` + `lens_cost_target_realization_test.rs` + `common/symbolic_cost_verification_fixture.rs`). **Q-Lens-Target-Context β-extended path DEFERRED** to N=2 trigger event (when second lens surfaces target-context need; emission_provenance most likely candidate per cross-cutting analysis); not active R3 ratification gate. | R2-Evaluator + R2-T-Substrate-Lens-Primitive + T-CostLens follow-on slice (Rust-side composition per ε) | α close at HEAD; #37 partial ε-slice; #40 + #70 integration receipts landed |
 | T-V2-Retirement | RED | `r3-tv2-*` briefs; PR #2334 PB Item 5 brief — encode #2068 P1 disposition (BinShimFilesSubsetPredicate) MERGED 2026-05-09 | T-FixedPoint + T-LensProducer | longest-path |
 | T-Free-Consequences-Demonstration | YELLOW | `r3-v-free-consequences-worker`; cycle PR-merge evidence (gate-promotion separate): PR #2495 (`auto_parallelism_independent_binds_emit_parallel` work) — partial evidence toward §1.8 #43 promotion. Per §1.8 canonical status: **#43 DECLARED** (PR #2495 merged but gate not yet promoted). T-Free's canonical demo-gate range is #43-#52 per `r3-structure.md` §"Lane structure"; upstream-lane PR-merge evidence (NOT credited to T-Free; tracked in their own rows per §1.8): #10/#33/#37/#40/#72 cycle merges all show similar PR-merged-not-yet-promoted patterns in their canonical lanes | R2-Evaluator + T-CostLens-Composition (advancing); residual demo gates #44-#52 DECLARED per §1.8 | post-deps; PR-merge evidence accruing for #43 awaiting status drift promotion |
 | T-E-P-Producer-Broadening | YELLOW | **PR #2528 [codex] Mark E-P producer coverage gate landed MERGED 2026-05-10**; foundational substrate work in flight; descent_evidence completeness driving cluster F | (foundational; in flight; coordinates with T-CostLens-Composition + T-Lens-Application-Surface) | weeks |