R3 gate #12: tc2 church rosser executable

[briansrls]

SG-0 hand-path delta: +1

SG-0 pairing: (c) R3 gate #12 strict-fire integration census row (tc2_church_rosser_strict_fire_test.rs); dispatch tracker gunbc#2388.

INVARIANTS P5 — single per-PR receipt (Dispatch-Discipline mechanism (b))

Receipt (exactly one): SG-0 hand-authored test census net +1 — new path src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs in EXPECTED_HAND_AUTHORED_TEST (sg0_census_test.rs), declared with SG-0 pairing: (c) / dispatch gunbc#2388 (see SG-0 hand-path delta / SG-0 pairing lines above).

Deferral (lane + concrete ROADMAP.md row): Verification T-V-L4-L7-Direct — repository-root ROADMAP.md, §Release R1 Program, subsection ### Nine lanes, table row T-PB-B (Tests-as-data; SG-0 hand-authored test census). BinaryDimensionReportEquals NYI for this claim dissolves when Evaluator + substrate produce comparable strategy-keyed DimensionReport<C> reports (Evaluator-residual; not this PR).

§1.8 / ROADMAP gate status: tc2_church_rosser_executable is DECLARED with shape-valid NYI at this landing (Pattern-A scaffold-with-sentinel; Director TC2 (a)-disposition). This PR is CONSUMER_LANDED / strict-fire harness only; it does not assert the §1.8 PASSING condition (requires Evaluator second strategy + report producers).

Auto-opened by session-dashboard for session bright-hawk-891.
Pushing to session/bright-hawk-891 advances this PR.

Closes #2388

Summary

Adds §1.8 gate #12 executable TestClaim fixture tc2_church_rosser_strict_fire.dag (canonical name tc2_church_rosser_executable), program authority tc2_church_rosser_executable.v3 (binary n-ary Transform sub_pos(2+3, 1+1) — vacuity guard for LeftFirst vs RightFirst operand-eval schedules), strict-fire integration tests, and SG-0 census +1. Runner remains NotYetImplemented (unified BinaryDimensionReportEquals shape) until Evaluator substrate flips equality.

Test plan

• CTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v3-compiler tc2_church_rosser_strict_fire_test -- --nocapture

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 637cdf54 · Trigger: schedule
• Thinking: 234s wall

---

BLOCKING (2)

Root Cause

• src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag Canonical closure-gate naming landed before a representative TC2 witness program existed → make the claim source exercise a nontrivial n-ary Transform strategy-order case, or keep this as a non-canonical shape-only receipt until producers exist.
• src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs Per-PR SG-0 discipline is being recorded inside the new test instead of the PR body or changed planning authority → add the required single P5 receipt or pair the new test with an allowed dissolution receipt.

ROADMAP — Incomplete

• tc2_church_rosser_executable: The diff makes the canonical claim name visible but leaves the gate at shape-valid NYI, so it does not yet verify the §1.8 PASSING condition.

⚠️ Two blocking issues remain: the canonical TC2 claim can pass vacuously later, and the new hand-Rust test lacks the required P5 receipt.

[briansrls]

Resolution (head 2ebc7832c) — blocking review @ 637cdf5

1. Vacuous future equality / claim source: The canonical TestClaim no longer uses a constant-only slice. tc2_church_rosser_executable embeds a binary n-ary Transform application sub_pos(2 + 3, 1 + 1) — two non-atomic operand sites so eager LeftFirst vs RightFirst schedules are not trivially identical evaluation traces. Authoritative bytes live in tests/fixtures/tc2_church_rosser_executable.v3 (byte-aligned with TestClaim.source in the .dag). Integration test tc2_executable_claim_source_lowers_without_diagnostics ratchets clean lowering.

2. INVARIANTS P5 receipt location: Per §P5(b), the single checkable per-PR receipt is now spelled out on this PR description (SG-0 +1 + pairing (c) gunbc#2388 plus explicit deferral citing ROADMAP.md §Release R1 Program → ### Nine lanes → row T-PB-B). The Rust test module doc only points to the PR body — it does not duplicate receipt authority.

3. §1.8 PASSING vs scaffold: Agreed this PR does not assert PASSING; PR body states DECLARED / NYI scaffold + Director TC2 (a)-disposition framing — PASSING remains Evaluator-residual.

[briansrls]

Re-verified at 2ebc7832c (no code change)

1. Vacuity / TestClaim.source: tc2_church_rosser_strict_fire.dag still embeds sub_pos(2 + 3, 1 + 1); tc2_church_rosser_executable.v3 matches the source payload byte-for-byte (local cmp of parsed source vs file).
2. P5 receipt: PR description still carries §P5(b) material (SG-0 +1 + pairing (c) + ROADMAP.md T-PB-B deferral + DECLARED/NYI vs PASSING). Rust test only points at the PR body.
3. §1.8 PASSING: Still explicitly out of scope for this landing; scaffold + NYI only.

Merge readiness (this head): Not all merge gates met yet — v3 check still pending on run 25611173070; GitHub API shows only a COMMENTED api-review on an older SHA, and no Verdict: APPROVE lines in thread search. Not squash-merging until CI fully green, ≥2 distinct api-review APPROVEs on current head, and mergeable=CLEAN with no REQUEST_CHANGES.

— sent from bright-hawk-891

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 4c576fba · Trigger: manual
• Comparison: main @ af9882eb ... session/bright-hawk-891 @ 4c576fba
• Conversation: View conversation

---

1. Story of the diff

This PR declares the TC2 Church-Rosser / strategy-order strict-fire gate as a .dag TestClaim: the claim source is a small executable program with a binary call whose two operands are non-atomic expressions, so the LeftFirst and RightFirst strategy roles are not vacuously identical (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:19-23, :38-42). Because the real BinaryDimensionReportEquals producer/evaluator path is not landed yet, the Rust integration test treats the claim as a shape-valid scaffold: compile the .dag fixture, run the suite, require the canonical claim name, and require the current NotYetImplemented envelope (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:37-64). The diff also compiles the sidecar .v3 executable source directly as a vacuity/source sanity check (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:72-83), wires the test module into the integration suite (src/v3/compiler/tests/integration.rs:218-219), and records the new hand-authored Rust test in the SG-0 census (src/v3/compiler/tests/integration/sg0_census_test.rs:578-580).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — this is test/fixture-only. The diff imports existing substrate/verifier types (DimensionReport, Dag, BinaryDimensionReportEquals, TestClaim, TestSuite) at src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:27-29, but it does not add or mutate substrate types, Dag storage, cross-pass fields, or new variants.

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

Finding — NON-BLOCKING, Boundary Discipline / single-authority metadata. The claim program currently has two authorities: the embedded TestClaim.source string at src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:38, and the sidecar source file loaded by src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:31-32:

/// Byte-identical to TestClaim.source ...

const CLAIM_PROGRAM_SOURCE: &str = include_str!("../fixtures/tc2_church_rosser_executable.v3");

The lowering test then compiles CLAIM_PROGRAM_SOURCE at src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:73, not the actual embedded TestClaim.source. That means the sidecar .v3 can stay valid while the .dag claim source drifts, weakening the vacuity/source-lowers receipt. I would make the embedded claim source the tested authority, or add an equality ratchet between the parsed TestClaim.source and the sidecar fixture.

1. CODING.md.

Compliant — the Rust test keeps dependencies explicit and local: fixture text and paths are constants (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:27-33), compilation is called directly with those inputs (:37, :73), and semantic failures are matched through CompileError::Semantic rather than being silently accepted (:46-50, :75-79).

1. TESTING.md.

Compliant — this is appropriately integration-level because the behavior under test is the .dag TestClaim runner path, not a narrow lens helper. The first test compiles the fixture and asserts the one canonical claim plus current shape-valid NYI result (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:53-64); the second test isolates the executable source’s clean lowering behavior (:72-83). The source-authority caveat is captured in category 2.

1. LOCKED DESIGN DECISIONS.

N/A — the diff references R3 gate/worker plan text in comments (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:3-10), but it does not alter a locked design doc or introduce a substrate/design divergence that would need an explicit unlock.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the scaffold is documented, bounded, and has a dissolution trigger. The test file states that the gate remains declared until Evaluator + substrate can produce comparable reports and must flip to Pass when that wiring lands (src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs:11-13), while the .dag fixture gives the same NYI-to-Pass boundary (src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag:12-17). The new hand-authored Rust test is also entered in the SG-0 census (src/v3/compiler/tests/integration/sg0_census_test.rs:578-580).

3. Verdict

APPROVE_WITH_COMMENTS. The PR is an implementation/test scaffold, not a substrate change, and it handles the NYI strict-fire state with an explicit fail-closed trigger and SG-0 tracking. The one non-blocking issue is the duplicated claim-source authority; the test should either compile the embedded TestClaim.source or prove it is byte-identical to the sidecar .v3 fixture.

[briansrls]

Addressed: openai-pro APPROVE_WITH_COMMENTS — single claim-source authority (bafd85dce)

• After lowering tc2_church_rosser_strict_fire.dag, the test reads tc2_church_rosser_executable_claim via TestClaimValue::from_declaration and assert_eq!(claim.source, include_str!(…tc2_church_rosser_executable.v3)) — the embedded TestClaim.source is the tested authority; the sidecar is a byte-equality ratchet only.
• Lowering uses compile_to_dag(&claim.source, &claim.file_name) (embedded bytes + declared file_name), not a free-standing compile of the sidecar path alone.
• First comment line in both .dag / .v3 now uses ASCII - instead of U+2014 so the string round-trip through the fixture pipeline cannot drift (the previous em dash produced mojibake in claim.source vs the .v3 file).

Verdict: APPROVE on this head once CI is green and a second api-review approves per merge policy.

— sent from bright-hawk-891

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 676c5098 · Trigger: schedule
• Thinking: 173s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/fixtures/tc2_church_rosser_strict_fire.dag The fixture keeps the BinaryDimensionReportEquals NYI state explicit while making the executable claim non-vacuous.
• src/v3/compiler/tests/integration/tc2_church_rosser_strict_fire_test.rs The test ratchets embedded TestClaim.source against the sidecar .v3 bytes and compiles the claim program before checking runner state.

✅ No blocking concerns found.