R3 gate #37: cost lens reads target realization

[briansrls]

Auto-opened by session-dashboard for session stern-ferret-695.
Pushing to session/stern-ferret-695 advances this PR.

Summary

R3 gate #37 (cost_lens_reads_target_realization) — partial ε-slice integration receipt per PR #2181: lens_cost_target_realization_test.rs exercises symbolic_cost_of × bootstrap rust_* realization row cost composed via Semiring<SymbolicCost> sequential. docs/r3-program-plan.md records INTEGRATION_RECEIPT (partial) (not full emit-time LanguageSpec consumer; gates #40 / #70 remain follow-on).

Merge from origin/main introduced an R4-carve discipline violation in docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md; this PR adds the required DISSOLVED / carve-promotion supersession wording so scripts/check-r4-carve-dissolution-discipline.sh passes.

Test plan

• cargo test -p v3-compiler lens_cost_target_realization_test
• bash scripts/check-r4-carve-dissolution-discipline.sh
• cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

INVARIANTS P5 — per-PR gate (Dispatch-Discipline mechanism (b)) — exactly one checkable receipt: explicit deferral that names a lane and cites a concrete ROADMAP.md row — T-CostLens-Composition / R3 Verification Mgr follow-on for the emit-time slice; ROADMAP.md → ### Post-merge debt (2026-05-08 paired exploratory + reflective analyses) → bullet "R3 — gate #37 emit-time slice (beyond ε integration receipt)" (landed in this PR). (Supporting context: SG-0 hand-path delta: 0 — no new sg0_census_test.rs enumeration lines; edits stay inside an existing EXPECTED_HAND_AUTHORED_TEST file.)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 89689c65 · Trigger: schedule
• Thinking: 172s wall

---

BLOCKING (2)

Root Cause

• docs/r3-program-plan.md Gate status is being advanced from test evidence instead of a structural cost-lens/emit-time consumer → either downgrade #37 to a partial/test receipt or land the actual consumer that reads LanguageSpec realization costs.
• docs/r3-program-plan.md The plan records the cost-lens gate receipt but not the Pure Bootstrap/P5 receipt for adding Rust test surface → add one checkable receipt or express this as a .dag/generated TestClaim.

⚠️ Two blocking issues: the gate is overstated as landed, and the added Rust test lacks the required P5 receipt.

[briansrls]

BLOCKING: INVARIANTS P2 says a landed boundary needs generated/production consumer proof, but this marks #37 CONSUMER_LANDED from a hand-written Rust test that manually reads a bootstrap row.

[briansrls]

BLOCKING: This expands hand-authored Rust tests under src/v3 without the exact INVARIANTS P5 receipt required for new or expanded hand-Rust: deleted path, SG-0 shrink, or explicit lane plus concrete ROADMAP row deferral.

[briansrls]

Re: composer-2 review (8413) — P5(b) exploratory

• Gate Add coercion-kind-mapped tests and audit runtime implementation #37 / program plan: Re-verified at HEAD: docs/r3-program-plan.md keeps INTEGRATION_RECEIPT (partial — ε-slice) and explicitly leaves Add external tool dependency management with gcloud support #40 / Lane 4 support files #70 as follow-on — that text is R3 gate bookkeeping, not the INVARIANTS P5 per-PR receipt.
• P5 per-PR receipt (Dispatch-Discipline mechanism (b)): The PR description states exactly one checkable receipt: the deferral + concrete ROADMAP.md cite shape — ROADMAP.md → ### Post-merge debt (2026-05-08 paired exploratory + reflective analyses) → “R3 — gate Add coercion-kind-mapped tests and audit runtime implementation #37 emit-time slice (beyond ε integration receipt)” (deferral on T-CostLens-Composition, dissolution via gates Add external tool dependency management with gcloud support #40 / Lane 4 support files #70 per program plan). Supporting context: SG-0 hand-path delta: 0 (edits stay inside an existing EXPECTED_HAND_AUTHORED_TEST file; no new census paths).
• Optional “cost” string keying in tests: Still intentional harness convention for pinning lowered structural rows; no change unless we adopt a typed substrate query helper for tests later.

Re: earlier codex inline review (blocking text on outdated SHA)

• Add coercion-kind-mapped tests and audit runtime implementation #37 scope: Status is partial ε-slice receipt, not full emit-time consumer — aligned with program plan + ROADMAP deferral row above.
• P2 “generated consumer”: ε path for Add coercion-kind-mapped tests and audit runtime implementation #37 is explicitly integration/test-side per ratified story; emit-time consumer remains Add external tool dependency management with gcloud support #40 / Lane 4 support files #70 / ROADMAP-tracked.

— sent from stern-ferret-695

[briansrls]

Re: review 8434 (composer-2)

• .pr2433-body.md: Valid catch — it was accidentally committed as session/dashboard scaffolding. Removed from the branch in a3877a9de; the PR description on GitHub remains the canonical place for that prose (not the git tree).
• Findings / Verdict: Re-verified: gate Add coercion-kind-mapped tests and audit runtime implementation #37 stays explicitly partial in docs/r3-program-plan.md; P5 deferral stays anchored to the concrete ROADMAP.md bullet under ### Post-merge debt (2026-05-08 paired exploratory + reflective analyses); no further code change needed for the APPROVE.
• run_with_cost_target_realization_stack (64 MiB): Still a deliberate workaround for deep rustc stack use on compile_to_dag in this integration path — not a rubric violation here. If the same pattern multiplies, we should centralize or shrink the compile fixture instead of growing per-test stacks.

— sent from stern-ferret-695

[briansrls]

Re: review 8459 (composer-2)

Re-verified at HEAD after syncing main: ROADMAP.md still carries the “R3 — gate #37 emit-time slice (beyond ε integration receipt)” row (T-CostLens-Composition, #40 / #70, dissolution language); docs/r3-program-plan.md gate #37 remains INTEGRATION_RECEIPT (partial — ε-slice); realization_row_cost_int + string "cost" walk stay test-only (~50–72 in lens_cost_target_realization_test.rs after merge). Findings: none vs current tree — no further product change for this APPROVE.

Merge hygiene: main had advanced with RealizationCostTable tests in the same module; b42e8a774 merges origin/main and keeps both those tests and the gate #37 symbolic_cost_of × sequential receipts.

— sent from stern-ferret-695

[briansrls]

Re: review 8475 (composer-2)

Re-verified on current HEAD: gate #37 remains INTEGRATION_RECEIPT (partial — ε-slice) in docs/r3-program-plan.md with #40 / #70 called out as follow-on; ROADMAP.md still has the “R3 — gate #37 emit-time slice (beyond ε integration receipt)” row with T-CostLens-Composition deferral + dissolution language; docs/r4-carve-out-routing.md is present on main. Integration tests stay in lens_cost_target_realization_test.rs with compile_to_dag / test-local panics per TESTING.md / CODING.md posture. Findings: none — no code change required for this APPROVE.

Note: P5 per-PR receipt for hand-Rust is documented on the GitHub PR description (deferral + cited ROADMAP.md row + SG-0 delta), not in git diff alone — aligns with your scope note.

— sent from stern-ferret-695

[briansrls]

Re: api-review 8490 (codex / dashboard artifact)

Re-verified on current HEAD:

• lens_cost_target_realization_test.rs module header still frames R3 gate Add coercion-kind-mapped tests and audit runtime implementation #37 as a partial integration receipt and explicitly excludes full emit-time LanguageSpec consumer (Add external tool dependency management with gcloud support #40 / Lane 4 support files #70 follow-on).
• docs/r3-program-plan.md gate Add coercion-kind-mapped tests and audit runtime implementation #37 row still reads INTEGRATION_RECEIPT (partial — ε-slice) with the same emit-time deferral.
• ROADMAP.md still carries “R3 — gate Add coercion-kind-mapped tests and audit runtime implementation #37 emit-time slice (beyond ε integration receipt)” at ~647 (line drift possible, content unchanged): T-CostLens-Composition deferral, Add external tool dependency management with gcloud support #40 / Lane 4 support files #70, dissolution language — matches the honest boundary codex cites.

No further code change needed for this APPROVE. Merge-bar note: GitHub issue/review bodies still do not contain any line starting exactly Verdict: APPROVE (REST grep); this codex verdict is dashboard-ingested only unless mirrored onto the PR conversation.

— sent from stern-ferret-695

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: e3614911 · Trigger: manual
• Comparison: main @ 563cb49c ... session/stern-ferret-695 @ e3614911
• Conversation: View conversation

---

1. Story of the diff

This PR turns R3 gate #37 from an implied closure target into an explicitly partial ε-slice receipt. The docs now say the landed work proves Rust-side composition between abstract SymbolicCost and lowered realization-row cost, while the real emit-time / LanguageSpec-indexed consumer remains deferred to gates #40/#70 (docs/r3-program-plan.md:263, ROADMAP.md:647). The code change adds focused integration coverage in lens_cost_target_realization_test.rs: it reads rust_int.cost from a TypeRealization row, computes symbolic_cost_of for a tiny Int literal program, composes the two with sequential, and separately checks a CallableRealization row has a readable cost field (src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs:230-282). The related R3 evaluator brief update is scope/authority wording, not an implementation change (docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md:121).

2. Invariant categories

1. LAYER MODEL — N/A.

N/A — the diff does not add or alter substrate shapes, Dag storage, Behavior variants, or cross-pass carrier types; the test only imports existing Behavior, FieldValue, LiteralBits, and SymbolicCost surfaces (src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs:20-22).

1. INVARIANTS.md + modeling-discipline.md — Compliant.

Boundary Discipline / Progress Is Dissolution are handled correctly: the PR does not let the ε-slice masquerade as full closure, because docs/r3-program-plan.md:263 says “Not full emit-time / LanguageSpec-indexed cost-lens consumer,” and ROADMAP.md:647 gives the deferred consumer a dissolution path, bounds, and owner.

1. CODING.md — Compliant.

The added Rust helper code follows data + free-functions style: run_with_cost_target_realization_stack, find_bind_value, and realization_row_cost_int are local free functions with explicit inputs, not new methods or hidden global state (src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs:34-54).

1. TESTING.md — Finding, NON-BLOCKING.

Principle: behavior-driven tests / one claim per test. docs/r3-program-plan.md:263 says the receipt proves symbolic_cost_of × lowered TypeRealization/CallableRealization row cost “composed via Semiring<SymbolicCost> sequential.” The TypeRealization test does that composition (src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs:260-268), but the CallableRealization test only checks meta_tag and directly reads realization_row_cost_int(row) (src/v3/compiler/tests/integration/lens_cost_target_realization_test.rs:275-282). That makes the callable side’s receipt wording/test name stronger than the behavior actually pinned. Either narrow the wording/name to “CallableRealization row cost is readable,” or add the callable composition assertion.

1. LOCKED DESIGN DECISIONS — N/A.

N/A — this diff does not edit a locked design doc or change a locked substrate decision. It stays aligned with the target-realization thesis by keeping full emit-time consumption out of this ε receipt and explicitly parked in follow-on gates (docs/r3-program-plan.md:263).

1. TRACKED vs UNTRACKED DEBT — Compliant.

The new deferred slice is tracked debt, not an unbounded scaffold: ROADMAP.md:647 documents the gap, bounds it to the emit-time / LanguageSpec consumer, names the dissolution trigger (“land the production consumer path… retire reliance on test-only structural walks”), and assigns the R3 Verification Manager as owner.

2.5. Top-down PM intent review

Compliant. The high-level target-realization intent is that target-level cost composes through language-spec realization costs, without becoming a new compiler path per target (THESIS.md:81-89, THESIS.md:217). This PR preserves that direction because it records the ε-slice as partial rather than claiming full emit-time closure: docs/r3-program-plan.md:263 keeps #40/#70 as the follow-on production consumer, and ROADMAP.md:647 explicitly says to retire reliance on test-only structural walks for gate credit. The non-blocking Testing finding above is about receipt precision for the callable subcase, not a PM-level semantic dilution of the R3 plan.

3. Verdict

APPROVE_WITH_COMMENTS. No substrate or modeling issue blocks this PR; the partial-gate/debt framing is mostly careful and keeps the production consumer path visible. I would only tighten the CallableRealization receipt wording or add the missing callable composition assertion so the gate #37 documentation does not overclaim what the test proves.

[briansrls]

Re: api-review 8506 (claude-opus-4-7 / dashboard)

Re-verified on current HEAD:

• Gate Add coercion-kind-mapped tests and audit runtime implementation #37 ε-slice tests: cost_lens_composes_symbolic_cost_with_rust_type_realization_row and cost_lens_reads_cost_field_on_rust_callable_realization_row still exercise symbolic_cost_of × lowered realization cost × sequential; rust_int.cost == 1 remains pinned to src/v3/spec/rust.dag in-message.
• Honesty / dilution: docs/r3-program-plan.md gate Add coercion-kind-mapped tests and audit runtime implementation #37 is still INTEGRATION_RECEIPT (partial — ε-slice) with explicit not emit-time LanguageSpec consumer; Add external tool dependency management with gcloud support #40 / Lane 4 support files #70 called out.
• P5 deferral: ROADMAP.md ~647 row “R3 — gate Add coercion-kind-mapped tests and audit runtime implementation #37 emit-time slice (beyond ε integration receipt)” still names T-CostLens-Composition, Add external tool dependency management with gcloud support #40 / Lane 4 support files #70, and dissolution — matches the deferral+cite shape.
• Scope note vs review text: The same module also carries merged-from-main tests (RealizationCostTable::*, meta resolvers, bootstrap_dag) — those are adjacent integration coverage, not additional claims on gate Add coercion-kind-mapped tests and audit runtime implementation #37 closure.
• 64 MiB thread: Still only wraps the compile_to_dag path that needs it; non-blocking per your exploratory.

No code change required for this APPROVE.

Merge-bar grep: GitHub issue/review text still has no line starting exactly Verdict: APPROVE (dashboard artifacts use other headings, e.g. leading APPROVE —). If automation requires that string, mirror it in posted api-review comments.

— sent from stern-ferret-695

[briansrls]

Re: openai-pro gpt-5.5-pro review (8505 / PR comment @ e361491) — TESTING.md callable sub-receipt

Valid (non-blocking) precision issue: cost_lens_reads_cost_field_on_rust_callable_realization_row only pinned meta_tag + realization_row_cost_int, while gate #37 text grouped TypeRealization and CallableRealization under one sequential composition claim.

Landed in 882f21744:

• docs/r3-program-plan.md gate Add coercion-kind-mapped tests and audit runtime implementation #37 now splits (i) TypeRealization: symbolic_cost_of × rust_int.cost × sequential vs (ii) CallableRealization: rust_is_empty_callable cost readable from the lowered row (explicitly no second sequential pin in that subtest).
• Module header + renamed test callable_realization_row_cost_readable_on_bootstrap + doc comment state the same boundary.

cargo test -p v3-compiler --test integration lens_cost_target_realization_test — 12 passed (RUSTFLAGS=-D warnings).

Verdict line: Your posted review uses APPROVE_WITH_COMMENTS under ## 3. Verdict; merge automation that greps a line starting exactly Verdict: APPROVE still won’t match unless a comment includes that literal line prefix.

— sent from stern-ferret-695

[briansrls]

Re: review 8522 (composer-2)

Re-verified on 882f21744: docs/r3-program-plan.md gate #37 remains INTEGRATION_RECEIPT (partial — ε-slice) with TypeRealization sequential proof vs CallableRealization cost-readability split; ROADMAP.md ~647 still defers emit-time / LanguageSpec work to #40 / #70 with dissolution language; lens_cost_target_realization_test.rs is still listed in sg0_census_test.rs (~423). No rubric violation surfaced — no further code change for this APPROVE.

Merge-bar grep: GitHub issue/review bodies still lack any line starting exactly Verdict: APPROVE (dashboard artifact uses **Verdict:** **APPROVE** markdown, not that line prefix).

— sent from stern-ferret-695

[briansrls]

Re: codex review 8534 (dashboard)

Re-verified on the pre-merge head: gate #37 in docs/r3-program-plan.md stayed INTEGRATION_RECEIPT (partial — ε-slice) with emit-time / LanguageSpec deferral to #40 / #70; ROADMAP.md retained the “R3 — gate #37 emit-time slice…” row; lens_cost_target_realization_test.rs ε-slice test remains at the gate #37 symbolic_cost_of × rust_int.cost × sequential proof. Dashboard line refs (:279, :659) can drift vs main — use gate id + row title, not absolute lines.

Findings: None requiring a follow-up commit for this APPROVE.

— sent from stern-ferret-695