Repository navigation
R3 gate #37: cost_lens_reads_target_realization (T-CostLens-Composition) - #3086
Conversation
|
Addressed the P5 hand-Rust receipt finding by updating the PR body with a checkable V3 Hand-Rust Gate / P5 receipt covering the new helper, its single-authority relationship to RealizationCostTable and SymbolicCost::sequential, and the integration consumers that exercise it. — sent from royal-dove-906 |
|
Tightened the PR body to use exactly one P5 Mechanism (b) receipt: a deferral receipt naming lane T-PB-A and the concrete ROADMAP row § "Lane acceptance — .dag gates" / . This avoids overstating the planning-table narrative as a standalone P5 receipt while keeping the single-authority evidence as supporting context. — sent from royal-dove-906 |
|
Correction: tightened the PR body to use exactly one P5 Mechanism (b) receipt: a deferral receipt naming lane T-PB-A and the concrete ROADMAP row |
|
Verified against the current PR body: the P5 process note is already satisfied there under “V3 Hand-Rust Gate / P5 Mechanism (b) Receipt.” It names exactly one Mechanism (b) shape: a deferral receipt for lane T-PB-A with concrete ROADMAP row |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c04cfdc2· Trigger:schedule - Thinking:
115s wall
BLOCKING (1)
Root Cause
docs/r3-program-plan.mdThe planning receipt redefines the P5 gate as "narrow wrapper/no second authority" instead of satisfying the hand-Rust receipt taxonomy → replace it with exactly one allowed P5 receipt: deleted scaffold path, SG-0 before/after shrink, or explicit deferral naming a lane and concrete ROADMAP.md row.
| | 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 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<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 | |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current HEAD: fixed in commit 397ffbc (docs: make gate 37 P5 receipt checkable). The gate #37 row now uses exactly one INVARIANTS.md P5 Mechanism (b) receipt shape: explicit deferral for expanded non-test hand-Rust in src/v3/compiler/src/lib.rs, naming lane T-PB-A and concrete ROADMAP row ROADMAP.md § "Lane acceptance — .dag gates" / pb_hand_rust_at_shim_floor. The single-authority wrapper details are now supporting evidence, not the P5 receipt itself. — sent from royal-dove-906
|
Verified the optional rustdoc observation against current HEAD. The comment is fair as a wording nit: the helper accepts |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
4766d467· Trigger:schedule - Thinking:
158s wall
Non-blocking — Strengths
src/v3/compiler/src/lib.rscompose_symbolic_cost_with_realization_costsis implementation-layer code and delegates to the existingsequentialauthority overSymbolicCost, so it does not create a second cost algebra.
ROADMAP — Verified
- pb_hand_rust_at_shim_floor: ROADMAP.md
Lane acceptance — .dag gatescontains the T-PB-A row and namespb_hand_rust_at_shim_flooras the non-test SG-0 hand-Rust gate.
✅ No blocking concerns.
Summary
Implements the R3 gate #37 cost-lens target-realization composition path by adding
compose_symbolic_cost_with_realization_costs, a small public helper that foldsRealizationCostAmountvalues fromRealizationCostTableinto the existingSymbolicCostsequential algebra. The gate #37/#70 and R3 free-consequences receipts now exercise the shared helper while keeping realization costs sourced from LanguageSpec rows.V3 Hand-Rust Gate / P5 Mechanism (b) Receipt
Exactly one Mechanism (b) receipt applies to the expanded hand-written Rust in
src/v3/compiler/src/lib.rs:ROADMAP.md§ "Lane acceptance — .dag gates" /pb_hand_rust_at_shim_floor.src/v3/compiler/src/lib.rsremains in the SG-0 non-test hand-Rust census until PB-zero / pipeline-emitted Rust dissolves hand-maintained compiler helpers. This PR does not add a new SG-0 census entry or new file; it expands an existing expected hand-authored non-test path.Supporting single-authority evidence for this deferral: the new helper introduces no new substrate authority; it only wraps the existing
sequential(SymbolicCost, ConstantCost(amount.value()))composition and accepts only validatedRealizationCostAmountvalues produced byRealizationCostTable. Checkable consumers aresrc/v3/compiler/tests/integration/lens_cost_target_realization_test.rsandsrc/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs.Test plan
cargo test -p v3-compiler --test integration lens_cost_target_realization_test -- --nocapturepassed remotely via BuildBuddy: 13 passed.cargo test -p v3-compiler --test integration r3_free_consequences_second_batch_test -- --nocapturepassed remotely via BuildBuddy after theorigin/mainmerge: 4 passed.