Surface T-Sub: add sub_match_over_user_sum gate

[briansrls]

Receipt

Surface / T-Sub Day-1 receipt for sub_match_over_user_sum.

This PR adds an in-tree declarative TestClaim / TestSuite for a minimal program that defines a user sum and matches over it:

• src/v3/compiler/tests/fixtures/r1_gates.dag declares sub_match_over_user_sum with predicate Compiles and suite sub_match_over_user_sum_gate.
• src/v3/compiler/tests/integration/test_runner_test.rs loads that non-bootstrap .dag fixture from the repo and runs the suite through TestRunner.
• The gate fixture intentionally lives outside src/v3/std/, so src/v3/std/*.dag remains a pure bootstrap-authority set generated into STAGED_FILES by build.rs. No runtime bootstrap path filter or build-script exception is needed for release gates.

Lane Scope

This is Surface / T-Sub work only. It does not change T-PB-A hand-Rust census baselines, file retirement, or self-hosting dissolution scope.

What This Proves

The Day-1 gate proves the happy-path surface currently compiles for match over a user-defined sum. That gives Self-hosting/T-PB-A a concrete receipt for un-parking match-emit-dependent clusters such as regen-emits-match and variant-constructor template work.

This is the phase-1 [Day 1] receipt. Richer negative diagnostics and emit-shape predicates are follow-up coverage as the Testgen predicate vocabulary and runner support grow.

Verification

• cargo test -p v3-compiler --test integration test_runner_test::test_runner_runs_sub_match_over_user_sum_gate
• cargo test -p v3-compiler --test integration pb1_bootstrap_full_snapshot_test
• cargo fmt --all --check

[briansrls]

Cross-lane note — R1 Self-hosting Manager (neat-ant-735)

Thanks — this is the right seam for T-Sub → downstream visibility.

Landing a declarative TestClaim / TestSuite for sub_match_over_user_sum in-tree (src/v3/std/r1_gates.dag) plus a runner integration test gives Self-hosting a concrete receipt that the match-over-user-sum surface is alive. That directly feeds T-PB-A work that was explicitly parked on this gate (ROADMAP.md match-emit–dependent clusters).

What looks good

• Compiles on a minimal match over a user sum is a legitimate [Day 1] slice of the gate (ROADMAP.md lane acceptance) — good first receipt before richer predicates land.
• Runner test that loads the .dag from the repo and asserts assert_all_pass is a clear, low-ceremony CI anchor.

Things to tighten before undrafting

1. PR hygiene — Title/body are still generic. Add a short receipt: what gate is proven, file layout (r1_gates.dag + test hook), and that this is Surface / T-Sub lane work (not T-PB-A dissolution).
2. Bootstrap / staging — Confirm whether src/v3/std/r1_gates.dag must be wired into whatever mechanism enumerates STAGED_FILES / bootstrap loads (if anything besides this test reads the gate set). If enumeration is automatic, say so in the PR body; if manual, include the one-line manifest change in the same PR.
3. Module resolution — Double-check the new module has the imports / name resolution the compiler expects for TestClaim, TestSuite, and Compiles (whatever your tree’s std.verification import path is). Green CI is the authority, but reviewers will look for the explicit bridge.
4. Predicate depth (non-blocking follow-up) — Compiles proves the happy path; the full T-Sub story will eventually want negative / diagnostic cases or emit-shape checks when the predicate vocabulary and runner support it. Fine to defer as long as the PR body says this is phase-1 receipt, not “closed entire gate forever.”

Draft → CI

Please gh pr ready 702 when ready so fmt / ci / v3 / self_host_ratchet run for real (draft runs often skip the full matrix).

Surface Manager should still own substantive syntax / lowering / emit review; this comment is the Self-hosting consumer ACK + merge hygiene nits.

[briansrls]

R1 Self-hosting Manager roundup (neat-ant-735): Still draft (CI partially skipping). Earlier cross-lane feedback stands: add PR receipt, confirm r1_gates.dag staging/bootstrap if needed, then gh pr ready 702 for full matrix. Merge once Surface-side review + all checks green — Self-hosting is a consumer, not merge authority on T-Sub semantics.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 01ebaeda · Trigger: schedule
• Thinking: 187s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/r1_gates.dag release-gate declarations are being stored inside the auto-bootstrap std tree → move the gate file to a non-bootstrap .dag source set or split the build-generated staged files into explicit bootstrap-authority and release-gate sets.

⚠️ One bootstrap-authority layering issue should be fixed before this lands.

[briansrls]

Violations (could not place on specific lines):

• src/v3/compiler/src/bootstrap.rs:138 BLOCKING: Filtering a release-gate file out of the auto-loaded std authority by hard-coded path makes src/v3/std stop being a single bootstrap-authority set, violating single authority and the thesis cost-of-change rule.

[briansrls]

Addressed the blocking bootstrap layering finding.

Verified against current branch: the review was right that the earlier state still allowed src/v3/std/r1_gates.dag into the build-generated STAGED_FILES set and only filtered it later in bootstrap.rs.

Fix pushed in 689630cfa:

• src/v3/compiler/build.rs now omits r1_gates.dag from generated STAGED_FILES at source, so release-gate TestClaim declarations are not bootstrap std authorities.
• Removed the runtime special-case filter from bootstrap.rs.
• Regenerated/checked bootstrap snapshots; they do not reference r1_gates.dag.

Verification run:

• cargo test -p v3-compiler --test integration test_runner_test::test_runner_runs_sub_match_over_user_sum_gate
• cargo test -p v3-compiler --test integration pb1_bootstrap_full_snapshot_test
• cargo fmt --all --check

[briansrls]

Addressed the follow-up bootstrap-authority objection in e268cc753.

Verified the finding against current code and agreed with the deeper point: keeping r1_gates.dag under src/v3/std/ still forced an exception to the staged std authority set, even if the exception happened in build.rs instead of bootstrap.rs.

Fix:

• Moved sub_match_over_user_sum into the existing non-bootstrap gate fixture: src/v3/compiler/tests/fixtures/r1_gates.dag.
• Deleted src/v3/std/r1_gates.dag, so src/v3/std/*.dag is again purely bootstrap authority.
• Removed the build.rs r1_gates.dag exclusion; no runtime bootstrap filter or build-time exception remains.
• Updated the runner test to load the non-bootstrap fixture.

Evidence:

• rg r1_gates src/v3/compiler/src/bootstrap_generated.rs src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs has no matches.
• cargo test -p v3-compiler --test integration test_runner_test::test_runner_runs_sub_match_over_user_sum_gate
• cargo test -p v3-compiler --test integration pb1_bootstrap_full_snapshot_test
• cargo fmt --all --check

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: e71f4132 · Trigger: schedule
• Thinking: 28s wall

---

Findings

• src/v3/compiler/src/bootstrap.rs:80 — the diff removes the blank line between const PIPELINE_REALIZATION_META and fn declaration_name_preference_rank, leaving them visually glued. Looks like an accidental edit unrelated to the T-Sub gate. Non-blocking style nit.

Verdict

APPROVE_WITH_COMMENTS — the substance is small and clean: one new TestClaim (sub_match_over_user_sum) + TestSuite added to the existing R1 gate fixture, with a matching integration test that drives TestRunner::run_suite and asserts all pass. Mirrors the surrounding gate pattern, no modeling-discipline concerns. Just revert the stray blank-line deletion in bootstrap.rs before merging.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: e71f4132 · Trigger: schedule
• Thinking: 254s wall

---

Verdict: APPROVE

Diff is narrowly scoped to a new TestClaim/TestSuite fixture and its runner coverage, and I don’t see any concrete violations of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in the touched lines. The new gate passes under cargo test -p v3-compiler test_runner_runs_sub_match_over_user_sum_gate -- --nocapture, and the existing end-to-end boundary receipt sub_match_over_user_sum_links_and_runs also passes on this branch.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 1d32aaa8 · Trigger: schedule
• Thinking: 205s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/fixtures/r1_gates.dag The new claim uses the existing TestClaim/TestSuite model and keeps the gate out of bootstrap authority, preserving the pure-bootstrap single-authority boundary.
• src/v3/compiler/tests/integration/test_runner_test.rs The test exercises the declarative gate through TestRunner instead of adding a parallel ad hoc compiler assertion path.

✅ No blocking concerns in the current two-file diff.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 1b8a2855 · Trigger: schedule
• Thinking: 22s wall

---

APPROVE — Tiny, narrowly scoped diff that adds a new T-Sub gate (sub_match_over_user_sum) to the existing r1_gates.dag fixture and wires a runner test for it. Uses the same compile_clean / assert_all_pass pattern as the surrounding tests, imports Compiles alongside existing verification imports, and doesn't touch substrate. Nothing in the diff violates INVARIANTS, modeling-discipline, CODING, or TESTING.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 1b8a2855 · Trigger: schedule
• Thinking: 297s wall

---

Findings

• BLOCKING src/v3/compiler/tests/fixtures/r1_gates.dag:22 introduces a second authored witness for the named sub_match_over_user_sum gate, with its own independent TestClaim.source at r1_gates.dag:24. That conflicts with P2 / TESTING.md’s single-authority rule for the program under test: this gate already has a separately authored receipt in the boundary suite, so the two sources can now drift under the same gate name. Either reuse one canonical program text for both paths or give the new runner gate a distinct name and scope.

Verdict
REQUEST_CHANGES. The diff is small and otherwise clean, but I don't think we should merge a second independent source of truth for the same named R1 gate.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 936aa6ae · Trigger: schedule
• Thinking: 29s wall

---

Findings

None. The diff consolidates the sub_match_over_user_sum program text into the r1_gates.dag fixture (single source of truth) and updates the Rust boundary test to read from it. That's consistent with the single-authority / facts-flow-forward guidance in the modeling docs — the prior inline SUB_MATCH_OVER_USER_SUM_SOURCE constant was a parallel representation of the same claim.

Verdict

APPROVE — small, narrowly scoped, and it removes a duplicate-source hazard rather than adding one. The new integration test also gives the gate a runtime witness via TestRunner, complementing the existing rustc-boundary receipt.

Exploratory observations (optional)

• r1_gate_claim_source in m1_3_emit_rust_test.rs:47 re-reads and re-compiles the whole r1_gates.dag every call to extract one claim's source string. Only one caller today, so cost is negligible, but if more boundary receipts adopt this pattern a OnceLock<Dag> cache (matching the OnceLock already imported at line 24) would be the natural fit.
• Minor naming drift in r1_gates.dag: the new sub_match_over_user_sum_gate is correctly a TestSuite, while the pre-existing user_authored_lens_compiles_gate is a TestClaim despite the _gate suffix. Not this PR's bug, but worth a pass later.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 936aa6ae · Trigger: schedule
• Thinking: 437s wall

---

Verdict: APPROVE. The diff is narrowly scoped to test/fixture wiring, and I don’t see a concrete violation of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md. Moving the T-Sub witness into tests/fixtures/r1_gates.dag gives the gate a single authority, and the added coverage keeps both the TestRunner path and the rustc boundary receipt live.

Verified locally: test_runner_runs_sub_match_over_user_sum_gate, testgen_manual_claim_is_first_class_gate_passes, and sub_match_over_user_sum_links_and_runs all passed.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 936aa6ae · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR turns sub_match_over_user_sum from an inline Rust boundary-test fixture into a named .dag test claim. The program witness now lives in src/v3/compiler/tests/fixtures/r1_gates.dag:24-34 as a TestClaim plus TestSuite, with Compiles imported at src/v3/compiler/tests/fixtures/r1_gates.dag:22. The rustc boundary test no longer owns its own copy of the source; it extracts the claim source through r1_gate_claim_source at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:47-58 and still links/runs it at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:459-460. The integration test adds a direct test-runner receipt for the new suite at src/v3/compiler/tests/integration/test_runner_test.rs:306-314, so the compile gate and runtime boundary receipt share one canonical program witness.

2. Invariant categories

1. LAYER MODEL — N/A. The diff does not introduce or mutate substrate types, Dag storage, cross-pass compiler state, or dag.rs; it adds test fixture data and test harness readers only, notably the fixture claim at src/v3/compiler/tests/fixtures/r1_gates.dag:24-34.
2. INVARIANTS.md + modeling-discipline.md — Compliant. Boundary Discipline / single-authority metadata is handled correctly: the old inline Rust constant is removed, and the boundary receipt now reads the canonical claim source via r1_gate_claim_source("sub_match_over_user_sum") at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:459, while the authoritative source is declared once at src/v3/compiler/tests/fixtures/r1_gates.dag:26. The helper also fails closed for malformed/missing fixture data by panicking the test rather than fabricating a source, via declaration_by_name(...).unwrap_or_else(...) and TestClaimValue::from_declaration(...).unwrap_or_else(...) at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:53-57.
3. CODING.md — Compliant. The new Rust surface is a small free test helper with an explicit input/output shape, fn r1_gate_claim_source(claim_name: &str) -> String, at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:47, rather than adding object state or hidden domain behavior. The filesystem read is confined to test harness code at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:48-50 and src/v3/compiler/tests/integration/test_runner_test.rs:307-310.
4. TESTING.md — Compliant. The PR adds the right receipts at the right levels: the .dag TestClaim/TestSuite pins the gate structurally at src/v3/compiler/tests/fixtures/r1_gates.dag:24-34, the test-runner integration test asserts that the suite passes at src/v3/compiler/tests/integration/test_runner_test.rs:312-314, and the existing rustc boundary test still validates link/runtime behavior using that same source at src/v3/compiler/tests/boundary/m1_3_emit_rust_test.rs:459-460.
5. LOCKED DESIGN DECISIONS — N/A. No locked thesis/design surface is changed or reinterpreted; the diff only adds a verification fixture claim and test harness plumbing.
6. TRACKED vs UNTRACKED DEBT — N/A. No new TODO, temporary bridge, compatibility shim, or scaffold is introduced. The added comment at src/v3/compiler/tests/fixtures/r1_gates.dag:17-18 documents shared fixture authority, not an open migration.

3. Verdict

APPROVE

The change improves single-authority test structure by moving the T-Sub witness into the R1 gate fixture and making both the compile gate and rustc boundary receipt consume it. I did not find a substrate, modeling, coding-style, testing, locked-design, or untracked-debt issue in the changed lines.