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

[briansrls]

SG-0 hand-path delta: +1

SG-0 pairing: (c) follow-up dispatch per docs/briefs/r3-substrate-t-costlens-composition-worker.md — interim symbolic_cost_verification_fixture.rs remains until testgen/substrate can author expected SymbolicCost literals for gate #40 dynamic oracles without a Rust surface serializer.

Auto-opened by session-dashboard for session sleek-ibex-570.
Pushing to session/sleek-ibex-570 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Summary

Lands T-CostLens-Composition gate #40 (symbolic_cost_expr_equals_executable) and gate #70 (cost_lens_demonstration) integration evidence: TestRunner + representative countdown/demo fixture, shared SymbolicCost→v3 literal serializer for dynamic oracles, fail-closed ClaimResult shape assertions, assert_recursive_countdown_linear_semantics on the gate #70 abstract cost, and SG-0 census + INVARIANTS.md receipt for the new common/symbolic_cost_verification_fixture.rs module. Updates docs/r3-program-plan.md §1.8 / lane row to match landed receipts.

Test plan

• cargo test -p v3-compiler symbolic_cost_expr_equals — pass
• cargo test -p v3-compiler sg0_census — pass
• cargo test -p v3-compiler cost_lens_demonstration_composes — pass
• cargo clippy -p v3-compiler --all-targets -- -D warnings — pass (local)

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: 59ca43f7 · Trigger: manual
• Comparison: main @ 86adc399 ... session/sleek-ibex-570 @ 59ca43f7
• Conversation: View conversation

---

1. Story of the diff

This PR turns SymbolicCostExprEquals from a previously declared/NYI-style verification predicate into an exercised integration receipt. It does that by adding a host-side helper that serializes runtime SymbolicCost values into v3 data …: SymbolicCost = … syntax, wiring that helper into integration test common exports, and adding #40 tests that prove the runner returns Pass for a representative countdown fixture and Fail rather than NotYetImplemented for type/value mismatches. The #70 side is narrower: it reuses the existing cost-target-realization fixture but routes the recursive-countdown linearity assertion through a shared helper, then updates docs/r3-program-plan.md, INVARIANTS.md, and SG-0 census receipts to mark the new Rust helper as tracked temporary test scaffolding with a dissolution path.

2. Invariant categories

1. LAYER MODEL — Compliant. This is implementation/test scaffolding plus planning-status updates, not a Dag substrate extension: the new surface is an integration helper in src/v3/compiler/tests/integration/common/symbolic_cost_verification_fixture.rs, and SG-0 explicitly records it as hand-authored test debt at sg0_census_test.rs:392 via the added path in pr-2785.diff:507-515.
2. INVARIANTS.md + modeling-discipline.md — Compliant. P5 tracked-debt discipline is handled: the new helper is recorded with documentation, bounds, and a named dissolution trigger in INVARIANTS.md:337, including “remove when TestClaim fixtures can declare expected SymbolicCost values … without a host-side serializer” in pr-2785.diff:9.
3. CODING.md — Compliant. The new helper is data + free functions rather than an object or hidden-state API: escape_v3_string_literal_content and symbolic_cost_as_v3_data_initializer are pure functions over explicit inputs at symbolic_cost_verification_fixture.rs:11 and :67 (pr-2785.diff:95, pr-2785.diff:151).
4. TESTING.md — Finding, non-blocking. The Add external tool dependency management with gcloud support #40 “representative recursive countdown” test is partly self-oracling: it computes the expected value with the same cost lens it is meant to exercise (let demo_cost = match symbolic_cost_of(&program, &demo_port) at m1_5_verification_test.rs:846, then let cost_init = symbolic_cost_as_v3_data_initializer(&demo_cost) at :850) and feeds that value back as the expected predicate input (predicate: SymbolicCostExprEquals(expected_demo_symbolic_cost) at :885; see pr-2785.diff:311-315 and pr-2785.diff:344-350). That is useful as an executable/serialization roundtrip receipt, but it is not an independent behavior-driven oracle for the representative countdown cost. I would either narrow the row wording to “roundtrip/executability receipt” or add one independent assertion for the expected abstract shape before treating this as semantic coverage.
5. LOCKED DESIGN DECISIONS — N/A. The diff does not alter a locked substrate/design decision; it updates R3 plan gate statuses and adds test scaffolding around an existing predicate.
6. TRACKED vs UNTRACKED DEBT — Compliant. The new hand-authored helper is tracked in both the SG-0 census and the INVARIANTS debt table: sg0_census_test.rs:392 adds the path with an inline comment naming why it exists and when it dissolves (pr-2785.diff:507-515), while INVARIANTS.md:337 adds the longer receipt (pr-2785.diff:9).

2.5. Top-down PM intent review

APPROVE_WITH_COMMENTS. The PR preserves the high-level direction: tests are moving toward .dag TestClaim receipts, and the new Rust helper is explicitly framed as a temporary bridge toward substrate/testgen-authored SymbolicCost literals rather than a permanent parallel authority. The only PM-level caveat is the same testing finding above: docs/r3-program-plan.md:266 now marks gate #40 as an INTEGRATION_RECEIPT based partly on symbolic_cost_expr_equals_countdown_demo_suite_passes (pr-2785.diff:35), but that countdown receipt derives its expected cost from symbolic_cost_of itself (pr-2785.diff:311-315). That can faithfully close “predicate executable + structural comparison path exists,” but it should not be read as an independent semantic proof of the countdown cost.

3. Verdict

APPROVE_WITH_COMMENTS. The PR is structurally disciplined: the new Rust test scaffold is tracked, bounded, and tied to a dissolution trigger, and the fail-closed predicate tests are real. My only comment is to avoid over-crediting the self-derived countdown fixture as an independent behavioral oracle; clarify the receipt wording or add an independent shape assertion.

[briansrls]

Addressed the openai-pro APPROVE_WITH_COMMENTS testing note on the representative countdown path: symbolic_cost_expr_equals_countdown_demo_suite_passes now pins independent unary tail-recursion semantics first (assert_recursive_countdown_linear_semantics on the countdown bind — same gate-#78 oracle used elsewhere), then runs the demo branch as an executability + v3 literal roundtrip receipt for SymbolicCostExprEquals / TestRunner. docs/r3-program-plan.md §1.8 row #40 wording was tightened to spell out that split so the row is not over-read as a purely self-derived semantic oracle for demo.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 59ca43f7 · Trigger: schedule
• Thinking: 302s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/tests/integration/common/symbolic_cost_verification_fixture.rs the helper assumes a string-escape syntax outside v3's actual StringEscapeSpec → align it to the tokenizer-supported escapes or return an explicit failure for unsupported characters.

⚠️ The PR is otherwise coherent, but the new SG-0 helper should not land with a silent source-rewriting path.

[briansrls]

BLOCKING: escape_v3_string_literal_content emits Rust-style \u{...} escapes that the v3 tokenizer does not decode, so valid TestClaim.source text containing other control whitespace is silently rewritten instead of failing closed (INVARIANTS P3).

[briansrls]

Verified the cursor/composer-2 dashboard review artifact (`/api/reviews/10412/artifacts/stdout.log`, 2026-05-12T21:02:06Z) against current `session/sleek-ibex-570` HEAD: Findings: None remains accurate. The diff still matches the described scope (SG-0 census + INVARIANTS receipt with named dissolution, gates #40 / #70, `docs/r3-program-plan.md` status text), and `escape_v3_string_literal_content` is aligned to v3 `StringEscapeSpec` with explicit panic for unsupported C0 controls (P3 fail-closed), not a silent rewrite path. No commit needed for this feedback item.

— sent from sleek-ibex-570

[briansrls]

Cross-checked cursor/composer-2 artifact `/api/reviews/10426/artifacts/stdout.log` (2026-05-12T21:18:10Z) against current `HEAD`:

• SG-0 / P5 pairing: `sg0_census_test.rs` lists `common/symbolic_cost_verification_fixture.rs` under `EXPECTED_HAND_AUTHORED_TEST` with an explicit dissolution note (testgen/reflection path); `INVARIANTS.md` row for the same path names §1.8 authority, dissolution aligned to `test_runner::field_value_to_symbolic_cost_eq_pattern`, and interim ratchet on serializer/escape alignment.
• Lane 4 support files #70 program-plan ↔ code: `docs/r3-program-plan.md` §1.8 row Lane 4 support files #70 cites `lens_cost_target_realization_test.rs::cost_lens_demonstration_composes_representative_rust_program_cost`; that test exists at the named path and wires `assert_recursive_countdown_linear_semantics` on the abstract carrier as described.
• Add external tool dependency management with gcloud support #40 harness / fail-closed: `m1_5_verification_test.rs` still carries the dynamic `SymbolicCostExprEquals` suite + `symbolic_cost_verification_fixture`; `escape_v3_string_literal_content` remains tokenizer-`StringEscapeSpec`-bounded with explicit panic for unsupported C0 controls (no silent rewrite).

Verdict concurrence: no blocking delta vs tree; optional golden-vector hardening is correctly scoped as follow-up, not this PR.

— sent from sleek-ibex-570