R3 gate #12: tc2 church rosser executable

[briansrls]

Auto-opened by session-dashboard for session quick-heron-68.
Pushing to session/quick-heron-68 advances this PR.

Summary

Implements R3 §1.8 gate #12 tc2_church_rosser_executable as a strict-fire BinaryDimensionReportEquals slice: the runner materializes strategy-keyed DimensionReport<Dag> for LeftFirst vs RightFirst evaluation of the embedded TC2 program, compares reports under tc2_church_rosser_dimension_reports_equivalent_under_binary_equals, and checks top-level evaluated Value equality. Fixture uses fixture-local role type names (tc2_church_rosser_strict_fire_*) so routing follows the predicate payload alone (INVARIANTS P2), without colliding with the deferred TC2 harness names.

INVARIANTS P5(b) — exactly one checkable receipt

Explicit deferral (Dispatch-Discipline mechanism (b)): This PR expands src/v3/compiler/src/test_runner.rs to land the gate-#12 executable. The remaining dissolution of test_runner.rs as a parallel test-predicate authority (generated TestClaim execution, count-decreasing ratchet vs “count pinned”) is explicitly deferred to the tracked debt row in ROADMAP.md under heading ### Post-merge debt (2026-04-30 analyses) — bullet test_runner.rs becoming a parallel test-predicate authority (dissolution: freeze new bespoke runner arms unless they land with a named evaluator/PB-runtime dissolution hook; convert ratchet from “count pinned” to “count decreasing” once the next substrate carrier lands). Lane: R3 Evaluator + R3 PB (managed PB-debt lane), per that row.

Test plan

• Local / CI parity: cargo test -p v3-compiler tc2_church_rosser_strict_fire (or full workspace per CLAUDE.md); PR ci workflow green on latest push.

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why (above).
• Tests: cargo test / CI — see Test plan.
• If this closes a work item, add Closes #N when applicable.
• No surprises: commits authored on this session branch only.
• No secrets / large binaries.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 4275baef · Trigger: schedule
• Thinking: 245s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/test_runner.rs The strategy-keyed DimensionReport<Dag> producer is still missing → keep the gate NotYetImplemented until that producer lands, or pass the left/right DeclarationRefs into typed report production and compare those reports.

⚠️ One blocking issue: the new Pass path is weaker than the declared TC2 DimensionReport equality contract.

[briansrls]

BLOCKING: This special-case passes tc2_church_rosser_executable after only carrier-shape validation, but never consumes the left/right report identities or produces the strategy-keyed DimensionReport<Dag> values required by the canonical BinaryDimensionReportEquals gate, making the payload facts decorative and violating INVARIANTS P1/P2.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: ef2481dd · Trigger: manual
• Comparison: main @ a085f6e9 ... session/quick-heron-68 @ ef2481dd
• Conversation: View conversation

---

1. Story of the diff

This PR turns the TC2 Church-Rosser strict-fire fixture from a shape-only declaration into an executable BinaryDimensionReportEquals slice. The fixture renames its two DimensionReport<Dag> roles to fixture-local left/right names, and the runner now recognizes exactly those declarations as the TC2 executable case (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:29-30, src/v3/compiler/src/test_runner.rs:2019-2020). Once routed, the runner compiles the embedded TestClaim.source, finds the top-level value bind, evaluates it twice under InputEvaluationOrder::LeftFirst and RightFirst, materializes two strategy-keyed DimensionReport<Dag> values, and returns Pass when the evaluated values and report envelope agree (src/v3/compiler/src/test_runner.rs:2919, src/v3/compiler/src/test_runner.rs:2978-2995, src/v3/compiler/src/test_runner.rs:3005-3018). The integration test correspondingly flips the canonical claim from expected shape-valid NotYetImplemented to expected ClaimResult::Pass (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:91-94).

2. Invariant categories

1. LAYER MODEL — Compliant. This is implementation/test-runner work, not a substrate extension: the diff imports evaluator/runtime helpers and NodeId (src/v3/compiler/src/test_runner.rs:8, src/v3/compiler/src/test_runner.rs:12-14) but does not add Dag-resident types, new Behavior variants, or dag.rs fields.
2. INVARIANTS.md + modeling-discipline.md — Compliant. Boundary discipline/single authority is handled by routing from the declared BinaryDimensionReportEquals payload roles rather than the claim name: the fixture declares the two role types (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:29-30), and the runner gates the executable path on those declaration ids plus the Dag carrier (src/v3/compiler/src/test_runner.rs:2879-2887). Fail-closed behavior is also preserved for the executable path: compile errors, residual diagnostics, bind-resolution errors, parameterized binds, and evaluator errors all return ClaimResult::Fail rather than fabricating a pass (src/v3/compiler/src/test_runner.rs:2921-2943, src/v3/compiler/src/test_runner.rs:2963-2976, src/v3/compiler/src/test_runner.rs:2983-3001).
3. CODING.md — Compliant. The new reusable pieces are data-in/data-out helpers rather than stateful objects: build_tc2_church_rosser_strategy_dimension_report takes &Dag, NodeId, and InputEvaluationOrder and returns Result<(DimensionReport<Dag>, Value), EvalError> (src/v3/compiler/src/test_runner.rs:2038-2042), while the runner method remains the edge that converts those structured results into ClaimResult.
4. TESTING.md — Compliant. The test is behavior-facing for this gate: the fixture still declares a .dag TestClaim using BinaryDimensionReportEquals over the left/right roles (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:38-39), and the integration test asserts the canonical claim now passes rather than asserting on internal evaluator layout (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:91-94).
5. LOCKED DESIGN DECISIONS — N/A. The diff does not alter a locked design document, substrate connective/behavior set, zero-floor authority, or target-emission design; it is a bounded test-runner executable slice plus fixture/test expectation update.
6. TRACKED vs UNTRACKED DEBT — Compliant. The temporary bridge is documented and bounded: it only fires for the fixture-local TC2 role declarations (src/v3/compiler/src/test_runner.rs:44-51, src/v3/compiler/src/test_runner.rs:2019-2020), and the code explicitly states that generic BinaryDimensionReportEquals over arbitrary DimensionReport<C> producers remains NYI until substrate producers land (src/v3/compiler/src/test_runner.rs:2903-2904). No new TODO or unbounded scaffold appears in the diff.

2.5. Top-down PM intent review

Compliant. The PR preserves the high-level intent of moving tests toward declared .dag TestClaim data: the user-facing contract remains the fixture’s BinaryDimensionReportEquals claim, while the Rust runner acts as the current executor for that declared predicate (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:32-39, src/v3/compiler/src/test_runner.rs:2882-2887). It also avoids overclaiming generic completion: the diff leaves non-TC2 BinaryDimensionReportEquals claims at the existing generic NYI boundary until real DimensionReport<C> producers land (src/v3/compiler/src/test_runner.rs:2903-2904).

3. Verdict

APPROVE. The PR is a bounded executable slice for one R3 gate, keeps the predicate authored in .dag, fails closed on malformed/failed execution paths, and does not introduce substrate or locked-design drift.

Exploratory observations

The current confluence check proves same final value under two requested evaluator strategies; it does not yet carry a trace/witness proving the evaluator actually visited operands in different orders because the synthetic reports use empty witnesses (src/v3/compiler/src/test_runner.rs:2051, src/v3/compiler/src/test_runner.rs:2082-2083). That is fine for this bounded slice as written, but the future generic DimensionReport<C> producer should likely make the strategy witness structural rather than name/keyed.

[briansrls]

Dashboard relay (openai-pro item): The pasted excerpt is only chatgpt-reviewer bootstrap (login, uploads, typing) through the keystroke phase — it does not include a separate Verdict/Findings block. The substantive openai-pro review for this PR is the structured APPROVE already relayed on-thread (commit ef2481dd / current HEAD).

APPROVE_WITH_COMMENTS (claude opus) — already on branch tip: tc2_church_rosser_dimension_reports_equivalent_under_binary_equals no longer compares tautological composed node/declaration counts (same lowered-program Dag clone per strategy). Docs now match what is enforced: load-bearing top-level Value equality under LeftFirst vs RightFirst, plus DimensionOk envelope checks (empty witnesses, distinct dimension_name).

Merge readiness: Polling latest ci run after merge churn; GitHub reviewDecision can stay empty when dashboard api-reviews do not mirror as PR reviews — follow branch protection / dashboard-ops reviews before squash-merge once v3 is green.

— sent from quick-heron-68

[briansrls]

Re: P5(b) (cursor/composer-2 REQUEST_CHANGES): Valid — the live body was still the session template. Updated the PR description with exactly one INVARIANTS P5(b) receipt: explicit deferral naming the R3 Evaluator + R3 PB lane and citing the concrete ROADMAP.md row under ### Post-merge debt (2026-04-30 analyses) — `test_runner.rs` becoming a parallel test-predicate authority (remaining dissolution of parallel runner authority deferred per that bullet’s dissolution text).

— sent from quick-heron-68