R3 gate #40: symbolic_cost_expr_equals_executable (T-CostLens-Composition)

[briansrls]

SG-0 hand-path delta: +1 (added src/v3/compiler/tests/integration/symbolic_cost_expr_equals_executable_ratchet_test.rs to EXPECTED_HAND_AUTHORED_TEST).
SG-0 pairing: (c) — structural deferral: dissolution lifts when the SymbolicCostExprEquals executable-wiring invariant is asserted by a .dag TestClaim / generated harness over src/v3/compiler/src/test_runner.rs (or its modeled successor) without this source-shape grep. Receipt row in INVARIANTS.md §"SG-0 hand-authored integration test receipts"; named follow-up dispatch: T-CostLens-Composition / R3 §1.8 gate #40 dissolution-tracking dispatch alongside adjacent T-CostLens hand-Rust receipts — queued brief docs/briefs/r3-substrate-t-costlens-composition-worker.md (Verification Mgr lane gunbc#2075).

Summary

Closes R3 §1.8 gate #40 symbolic_cost_expr_equals_executable (T-CostLens-Composition) via a mechanical fail-closed ratchet on the SymbolicCostExprEquals executable wiring in src/v3/compiler/src/test_runner.rs, and promotes the §1.8 row status from INTEGRATION_RECEIPT → CONSUMER_LANDED + PASSING.

Wider end-to-end pass + fail-closed receipts for the predicate (smoke + countdown demo + type/value mismatch fail-closed) already live in m1_5_verification_test.rs (symbolic_cost_expr_equals_smoke_suite_passes, symbolic_cost_expr_equals_countdown_demo_suite_passes, symbolic_cost_expr_equals_fail_closed_*). This PR adds a focused NYI-shell-retirement ratchet pinning the dispatch arm + evaluator wiring, so accidental retirement back to the NotYetImplemented shell trips at test time rather than in downstream consumers — matching the gate-#39 ratchet-test pattern (sibling PR #3088).

Changes

• src/v3/compiler/tests/integration/symbolic_cost_expr_equals_executable_ratchet_test.rs (new) — two fail-closed tests:
  • symbolic_cost_expr_equals_dispatch_arm_is_wired_in_test_runner — verifies the "SymbolicCostExprEquals" => dispatch arm + eval_symbolic_cost_expr_equals_shape evaluator both exist in test_runner.rs.
  • symbolic_cost_expr_equals_evaluator_does_not_return_not_yet_implemented_shell — bounds-scans the evaluator body and asserts the generic TestPredicate::{other} is not wired in the Rust runner yet NotYetImplemented shell is not present.
• src/v3/compiler/tests/integration.rs — wires the new module (sorted slot between shape_a_… and t_ci_…).
• src/v3/compiler/tests/integration/sg0_census_test.rs — adds the ratchet path to EXPECTED_HAND_AUTHORED_TEST (sorted-ASCII slot).
• INVARIANTS.md §"SG-0 hand-authored integration test receipts" — new receipt row with dissolution posture + interim ratchet test names (P5 Mechanism (b) home-of-record).
• docs/r3-program-plan.md §1.8 row Add external tool dependency management with gcloud support #40 — promoted to CONSUMER_LANDED + PASSING.

Test plan

• cargo test -p v3-compiler --test integration -- symbolic_cost_expr_equals_executable_ratchet sg0_census → 18 passed; 0 failed (incl. the 2 new ratchet tests + sg0 sort/uniqueness).
• cargo test -p v3-compiler --test integration -- symbolic_cost_expr_equals (in m1_5_verification_test) → 4 passed; 0 failed (smoke + countdown demo + 2 fail-closed cases) — pre-existing receipts remain green at HEAD.

Closes node://adhoc-e9cd1fed-fff.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

[briansrls]

Addressed in 32701b9: added the SG-0 receipt row in INVARIANTS.md for src/v3/compiler/tests/integration/symbolic_cost_expr_equals_executable_ratchet_test.rs (slot between r3_gate_60_* and t_gate_58_*), citing R3 §1.8 gate #40, dissolution posture, and both interim ratchet test names. Pattern follows adjacent T-CostLens receipt rows. The exploratory note on source-shape sensitivity is acknowledged and reflected in the row's dissolution posture (lifts when a .dag/generated harness can assert the same wiring invariant without grep).

— sent from vivid-crab-673

[briansrls]

Acknowledged — and intentional trade-off, not a replacement for the behavior tests.

The two existing m1_5_verification_test.rs receipts (symbolic_cost_expr_equals_smoke_suite_passes + symbolic_cost_expr_equals_countdown_demo_suite_passes + the symbolic_cost_expr_equals_fail_closed_* cases) are the behavior-first runner-interface receipts you describe — they exercise SymbolicCostExprEquals end-to-end through TestRunner::run_suite and assert on ClaimResult::Pass / ClaimResult::Fail (explicitly not NotYetImplemented). Those receipts are cited as the canonical seam in both the §1.8 row #40 promotion to CONSUMER_LANDED + PASSING and the new INVARIANTS.md SG-0 row.

The new symbolic_cost_expr_equals_executable_ratchet_test.rs file is deliberately a complementary source-shape tripwire targeting the specific regression class gate #40's predicate names — accidental retirement of the dispatch arm back to the generic TestPredicate::{other} is not wired in the Rust runner yet NotYetImplemented shell. That shell-retirement is the exact transition the gate predicate ratchets away from (see docs/r3-structure.md:115), and it survives behavior-first end-to-end suites silently if a future edit ever drops the "SymbolicCostExprEquals" => dispatch arm while keeping the evaluator function compiled (the suite would then fail-closed in a confused way rather than naming the regression class).

The INVARIANTS.md SG-0 row encodes this as an explicit interim ratchet with a named dissolution trigger: "remove when the SymbolicCostExprEquals executable-wiring invariant is asserted by a .dag TestClaim / generated harness over src/v3/compiler/src/test_runner.rs (or its modeled successor) without this source-shape grep — same dissolution posture as adjacent T-CostLens hand-Rust receipts." The cursor review's exploratory note on the same trade-off was explicitly OK'd as "acceptable here if treated as an explicit interim ratchet until a structural receipt exists" — the SG-0 receipt + INVARIANTS row carry that posture.

So: behavior-first surface = the m1_5_verification_test.rs suite (already landed, cited as the §1.8 receipt). Source-shape ratchet = this PR's small tripwire (named, interim, with explicit dissolution). Treating them as a single "authority" would conflate the two — the SG-0 receipt row keeps them distinct and named.

— sent from vivid-crab-673

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 32701b97 · Trigger: schedule
• Thinking: 195s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/integration/symbolic_cost_expr_equals_executable_ratchet_test.rs The new test is implementation-layer only, has a bounded dissolution path, and leaves behavioral pass/fail-closed coverage with the existing m1_5 verification receipts.

ROADMAP — Verified

• R3 gate #40 symbolic_cost_expr_equals_executable: The changed plan row, SG-0 census line, and INVARIANTS receipt consistently track the temporary Rust ratchet to T-CostLens-Composition.

✅ No blocking concerns.

[briansrls]

Addressed in d55bd0c: replaced the source-text grep with two behavior-driven TestRunner tests:

• symbolic_cost_expr_equals_well_shaped_claim_never_returns_not_yet_implemented — compiles a minimal SymbolicCostExprEquals TestClaim, runs through TestRunner::run_suite, and forbids ClaimResult::NotYetImplemented(_) (the dispatch-fallthrough shell gate Add external tool dependency management with gcloud support #40 ratchets away from).
• symbolic_cost_expr_equals_malformed_expected_returns_fail_not_not_yet_implemented — exercises the dedicated evaluator's typed-shape rejection (expected typed as Int, not SymbolicCost) and asserts the runner returns Fail(_), never NotYetImplemented(_).

Both tests pin the dispatch arm indirectly through runner behavior: a regression to the generic TestPredicate::{other} is not wired in the Rust runner yet fallthrough trips the first test (where the well-shaped claim should Pass) and is robust to dispatch reshaping, helper renames, and message-text edits — the source-text spellings, indentation anchors, and substring windows from the prior version are gone. INVARIANTS.md SG-0 receipt row updated to cite the new test names.

— sent from vivid-crab-673

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ae9f4d3f · Trigger: schedule
• Thinking: 227s wall

---

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/r3-program-plan.md The row #40 PASSING update is backed by the TestRunner ratchet, but ROADMAP.md still carries the open SymbolicCostExprEquals-NYI debt row; retire or close that row here, or defer under T-CostLens-Composition.

ROADMAP — Incomplete

• symbolic_cost_expr_equals_executable: The PR syncs the R3 plan, INVARIANTS receipt, and SG-0 census entry, but the ROADMAP debt row still needs a closed/retired receipt.

✅ No blocking concerns.