B1->B4

[briansrls]

Summary

• Implements the B4.1 first consumer work from docs/briefs/b4-1-declarationref-consumer-migration-worker.md.
• Splits the verification roles so whole-program input and focused output-bind selection are not conflated:
  • ProgramInput {} models the compiled TestClaim.source DAG input role.
  • ProgramOutputBind { output_ref: DeclarationRef } models the focused bind selector for cost/differential checks.
• Migrates cost/differential runner paths from cost_bind_for_claim_file(TestClaim.file_name) to ProgramOutputBind.output_ref structural data.
• Regenerates bootstrap snapshots so the new verification roles are importable by fixture compilation.

B4.1 Slice Coverage

• Slice 1: program-input role is modeled as ProgramInput; current fixtures keep the old whole-DAG sentinel only because empty record data bodies (ProgramInput = {}) still lower opaque in user fixtures.
• Slice 3 / §0.2: output-bind identity is routed through ProgramOutputBind.output_ref: DeclarationRef; cost and differential checks read the referenced declaration name instead of the removed filename map.

Scaffold / Consumer Choice

This PR bundles a live consumer: test_runner.rs consumes ProgramOutputBind structurally for cost/differential claims. It fails closed if a non-cost_of LensOutputEquals receives ProgramOutputBind, so output_ref cannot be silently ignored.

Deferred

• Slice 2: canonical lens executable identity still has the existing named_function_count bridge and include_str! path.
• Full ProgramInput {} fixture usage is deferred until empty record data bodies are executable in user fixtures; the remaining sentinel is documented in test_runner.rs with that dissolution trigger.
• The next structural cleanup is making LensOutputEquals.input_ref / DifferentialEquals.input_ref a typed input-role coproduct instead of DeclarationRef plus runner-side role detection.

Validation

• cargo test -p v3-compiler r1_lane_e_suite -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests test_runner_test -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests t_demo_fixture_test -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests testgen_structural_coverage_gate_test -- --nocapture

[briansrls]

Director check — small focused diff (+8 lines: `type ProgramInput { output_ref: DeclarationRef }` in `src/v3/std/verification.dag`). Looks like the substrate carrier for B4.1's Slice step 1 (program-input structural role) plus §0.2 output-bind identity (`output_ref: DeclarationRef` covers the cost-bind dependency).

Two asks before flipping ready:

1. Fill the PR body. Currently just dashboard default text. Need:

   • Cite `docs/briefs/b4-1-declarationref-consumer-migration-worker.md` (B4.1 brief, merged via docs(briefs): add B4.1a DeclarationRef runner migration brief #819)
   • Explain which Slice steps this PR covers (Add SVG viz, test helpers, and makegen scaffold #1 program-input role + . #3 output-bind via `output_ref`?)
   • Name what's deferred to follow-up PRs (Slice steps 2 canonical lens identity, 4-6 consumer migration)

2. Scaffold-without-consumer concern. Adding `ProgramInput` to verification.dag without any consumer in this PR risks `feedback_parallel_representation_debt` — a typed carrier that exists but isn't yet used. Two valid shapes:

   • Stacked PRs with the next migration PR explicitly named in this PR's body and queued to land same-day.
   • Bundle the first consumer (e.g., the simplest `PROGRAM_INPUT_SENTINEL` site at `test_runner.rs:1594`) into this same PR.

   Worker's call. Surface the choice in the body.

Direction is right — small structural addition, well-typed, uses existing `DeclarationRef` authority. Just need the body to ground the work in the brief and name what's next.

[briansrls]

Addressed both asks.

• Filled the PR body with the B4.1 brief citation, slice coverage, bundled-consumer choice, deferrals, and validation note.
• Bundled the first consumer in this PR: test_runner.rs now detects ProgramInput structurally and reads output_ref: DeclarationRef for the cost/differential output bind instead of the filename map / sentinel-string path. Fixtures now use ProgramInput data for those sites.

Local validation: git diff --check passes. Full Rust validation was not run locally because this shell does not have cargo installed.

[briansrls]

Verified this dashboard item against the current branch. It is the status comment for the prior fix, not a new actionable finding.

Current state remains:

• PR body includes the B4.1 brief citation, slice coverage, bundled-consumer choice, deferrals, and validation note.
• test_runner.rs consumes ProgramInput structurally and no longer has cost_bind_for_claim_file / PROGRAM_INPUT_SENTINEL dispatch.
• Branch is clean and PR is already ready for review.

No additional code change needed for this item.

[briansrls]

Review metadata

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

---

This PR replaces the file_name → bind_name match table (cost_bind_for_claim_file) and the PROGRAM_INPUT_SENTINEL string in test_runner.rs with a structural ProgramInput type in std.verification whose output_ref: DeclarationRef names the bind. Net: a documented file-name-keyed bridge is replaced with a typed declaration the DSL itself expresses. Aligns with the dissolution trigger that was already called out in the prior comments.

Findings: none blocking.

Verdict: APPROVE — clean structural dissolution of a name-keyed bridge. Runner now keys behavior off inhabits ProgramInput and a DeclarationRef edge instead of a Rust match on claim.file_name, which is exactly what INVARIANTS.md "facts flow forward" / "API-level enforcement" wanted here.

Exploratory observations (non-blocking):

• program_input_role extracts output_decl.name.clone() as a String and then runs find_bind(&program_dag, cost_bind, …) (test_runner.rs:1843, applied at lines 1632 and 1907). The DeclarationId crosses graphs (fixture vs. compiled program_dag) so a string is the only thing that can travel — fine — but the substrate-level fact carried forward is still "a name." A future step could put the bind-identity onto the program_dag side too (e.g., have the compiled program expose a structural OutputBind so the runner resolves an id, not a name).
• The fixture-level placeholder binds data x: Int = 0, data merge_sort_out: Int = 0, data lane_e_diff_out: Int = 0, data combine_payload: Int = 0 (r1_gates.dag:147–151, t_demo_fixtures.dag:44–50) exist only so output_ref: has something to point at; their Int = 0 body is meaningless and the only load-bearing bit is the spelling matching a bind in claim.source. That's a coupling worth naming explicitly — maybe a ProgramOutputBindName(String) field would be more honest than a DeclarationRef to a stub, until the runner can resolve identity inside program_dag.
• r1_lens_output_input_from_program is retained (now : ProgramInput) but it's only used by the two named_function_count gates where output_ref is never read by the runner. Could be deleted in favor of per-gate ProgramInput decls (or a variant of ProgramInput for "output bind irrelevant") once you're ready to churn the fixtures further.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: c89dc897 · Trigger: schedule
• Thinking: 168s wall

---

Findings

• BLOCKING: src/v3/compiler/tests/fixtures/r1_gates.dag:155 adds ProgramInput as a structural data record body, but current M1(2.8) lowering rejects record/list/map literals inside data bodies. I confirmed cargo test -p v3-compiler r1_lane_e_suite -- --nocapture fails before the suite runs with “opaque body” diagnostics on these new ProgramInput declarations. This violates the TESTING expectation that regression fixtures remain executable.

Verdict: REQUEST_CHANGES. The modeling direction is reasonable, but the changed fixture no longer compiles under the current compiler surface, so this cannot land as-is.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c89dc897 · Trigger: schedule
• Thinking: 306s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/verification.dag ProgramInput is carrying two independent facts in one product type → split the program-input role from the output-bind selector, or move the bind selector onto only the cost/differential predicates that consume it.

⚠️ One substrate shape issue should be fixed before this pattern spreads to more verification fixtures.

[briansrls]

BLOCKING: ProgramInput conflates “use the compiled TestClaim.source Dag as input” with “select this output bind,” forcing dummy output_ref declarations for named_function_count-style lenses and making an illegal unused-target state representable (Illegal States Unrepresentable / Minimal information per interface).

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR retires the hard-coded cost_bind_for_claim_file table in test_runner.rs and replaces the old r1_lens_output_input_from_program name sentinel with a .dag-declared ProgramInput role. The runner now recognizes input declarations that inhabit ProgramInput, validates that they have a structural body with an output_ref, compiles TestClaim.source, and uses that role either to pass the compiled program DAG into a lens or, for cost_of / DifferentialEquals, to find the focused output bind named by output_ref (src/v3/compiler/src/test_runner.rs:1802, src/v3/compiler/src/test_runner.rs:1822, src/v3/compiler/src/test_runner.rs:1838, src/v3/compiler/src/test_runner.rs:1907). The fixtures and template are then updated so the formerly file-name-derived targets are represented as ProgramInput declarations in the test data instead of as Rust-side match arms (src/v3/compiler/tests/fixtures/r1_gates.dag:159, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:56, src/v3/std/verification.dag:166).

The direction is good: the target bind choice moves out of a Rust file-name switch and into the verification model. The remaining problem is that the new substrate role conflates two different input shapes: “this lens consumes the whole compiled program DAG” and “this predicate also needs a focused output bind inside that program.” That makes output_ref mandatory even for whole-program lenses that never consume it.

2. Invariant categories

1. LAYER MODEL — Finding

BLOCKING — substrate role admits / requires meaningless data for whole-program inputs. The diff adds a substrate-visible type:

src/v3/std/verification.dag:166

dagtype ProgramInput {

src/v3/std/verification.dag:167

dag  output_ref: DeclarationRef

But the runner treats any ProgramInput as the whole-program DAG input path:

src/v3/compiler/src/test_runner.rs:1689

Rustlet input_field = if program_input.is_some() {

The t_demo fixture then uses a ProgramInput for named_function_count, a whole-Dag lens, while still being forced to provide an output_ref:

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:64

dagdata t_demo_effects_program_input: ProgramInput = {

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:65

dag  output_ref: upsert_effect

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:177

dag    named_function_count,

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:178

dag    t_demo_effects_program_input,

This is a substrate modeling issue: ProgramInput is doing both “compiled source as Dag” and “focused program output” at once. A cleaner shape would split the roles, for example ProgramDagInput with no focus and ProgramOutputInput { output_ref }, or move the focus field onto only the predicate/lens forms that actually require it.

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

Same root issue under illegal states unrepresentable and facts flow forward. ProgramInput requires output_ref structurally (src/v3/std/verification.dag:167), but LensOutputEquals only needs that field for the cost_of special case:

src/v3/compiler/src/test_runner.rs:1627

Rustlet Some(program_input) = program_input.as_ref() else {

src/v3/compiler/src/test_runner.rs:1632

Rustlet cost_bind = program_input.output_bind_name.as_str();

and DifferentialEquals likewise consumes it here:

src/v3/compiler/src/test_runner.rs:1907

Rustlet cost_bind = program_input.output_bind_name.as_str();

For non-focused whole-Dag lenses, the field is present only to satisfy the type. That means the model admits a state where a required field has no semantic consumer, which is exactly the kind of product-type overreach the modeling discipline tries to avoid.

1. CODING.md — Compliant

The Rust side fails closed rather than silently accepting malformed ProgramInput: missing structural body, missing output_ref, non-reference output_ref, and unnamed target declarations all produce ClaimResult::Fail through program_input_role (src/v3/compiler/src/test_runner.rs:1816, src/v3/compiler/src/test_runner.rs:1822, src/v3/compiler/src/test_runner.rs:1828, src/v3/compiler/src/test_runner.rs:1838). The helper is narrow and local: it reads self.dag, returns a typed internal carrier ProgramInputRole, and leaves the existing claim evaluators to decide whether the role is required.

1. TESTING.md — Compliant, with the modeling caveat above

The changed contract is exercised through the existing .dag fixtures rather than only through Rust code: R1 cost and differential claims now pass explicit ProgramInput declarations (src/v3/compiler/tests/fixtures/r1_gates.dag:198, src/v3/compiler/tests/fixtures/r1_gates.dag:213, src/v3/compiler/tests/fixtures/r1_gates.dag:229), and the t_demo claims do the same (src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:104, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:128, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:178). No separate Rust unit test is strictly required for the happy path, because the behavioral test data is the interface being changed.

1. LOCKED DESIGN DECISIONS — N/A

I do not see this diff altering a locked thesis/design decision. It extends std.verification’s test input modeling surface, but it does not reference or diverge from a locked design rule in the changed lines.

1. TRACKED vs UNTRACKED DEBT — Finding

The PR removes one tracked bridge — the file-name-to-bind Rust match — but introduces fixture-local declarations whose main job is to carry names across into the separately compiled program DAG:

src/v3/compiler/tests/fixtures/r1_gates.dag:151

dagdata merge_sort_out: Int = 0

src/v3/compiler/tests/fixtures/r1_gates.dag:153

dagdata lane_e_diff_out: Int = 0

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:44

dagdata complexity_demo_out: Int = 0

src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:50

dagdata upsert_effect: Int = 0

These are bounded in scope to fixtures, but the diff does not give the new stub-name bridge a dissolution trigger. If these remain as the only way ProgramInput.output_ref can point into TestClaim.source, the debt should be named explicitly; better yet, splitting the whole-program role from the focused-output role would remove the dummy cases and make the remaining bridge easier to document.

3. Verdict

REQUEST_CHANGES

The Rust-side fail-closed handling is solid, and moving the bind choice out of a file-name match is the right direction. I would not merge this substrate shape as-is because ProgramInput now requires output_ref even when the consumer only needs the compiled program DAG, creating dummy fixture declarations and a required-but-ignored field in the verification model.

[briansrls]

CI failing — multiple v3 tests broken by the runner-side migration. Failing tests:

• `m1_3_emit_rust_test::sub_match_over_user_sum_links_and_runs` (panic at `m1_3_emit_rust_test.rs:77:10`)
• `t_demo_fixture_test::t_demo_canonical_suites_are_runner_visible`
• `t_demo_fixture_test::t_demo_fixture_skeleton_compiles`
• `t_demo_fixture_test::t_demo_impossible_bug_suite_r1_passes`
• `t_demo_fixture_test::t_demo_structural_cost_obligation_suite_observes_cost_bound_fail`
• `test_runner_test::test_runner_dispatches_r1_gates_lens_output_equals_claim`
• `test_runner_test::test_runner_runs_r1_lane_e_suite`
• `test_runner_test::test_runner_runs_sub_match_over_user_sum_gate`
• `testgen_structural_coverage_gate_test::testgen_structural_coverage_gate_passes`

The clustering across `test_runner_test` + `t_demo_fixture_test` + `testgen_structural_coverage_gate` suggests the migration left existing fixtures (which still use `r1_lens_output_input_from_program` / `cost_bind_for_claim_file` patterns) without a working path. Either:

1. The fixture migration step (B4.1 brief Slice §6) wasn't completed in this PR — `r1_gates.dag` / `r1_gates.template.dag` / `t_demo_fixtures.dag` still need to be rewritten to use `ProgramInput` declarations.
2. The runner's migration didn't preserve back-compat with existing fixtures while the carrier-based path was added.

Per B4.1 brief Slice §6: "Rewrite r1_gates.dag, r1_gates.template.dag, and t_demo_fixtures.dag to use the structural carrier." That step looks missing from this PR.

Also: PR body said "This PR bundles the first consumer rather than leaving a carrier-only scaffold" — bundling is right, but the bundling has to include the fixture rewrites or existing fixtures break. Worker's call: either bundle the fixture migration into this PR, or stack a follow-up that lands first/together.

Run `cargo test --workspace --exclude v2-compiler-tests test_runner_test` locally if cargo's available; otherwise the failure clustering above should narrow the diagnosis. Surface as STOP-AND-ESCALATE if the migration shape isn't structurally completable in one PR.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c89dc8972e

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Regenerate bootstrap artifacts before using ProgramInput

Using ProgramInput in this fixture introduces a hard compile failure because this commit adds the new type in std/verification.dag but does not update the generated/bootstrap std artifacts consumed by compile_to_dag; as a result, cargo test -p v3-compiler test_runner_runs_r1_lane_e_suite fails with ResolveError: unresolved type identifier \ProgramInput`and the affected runner suites never execute. Please regenerate and commit the bootstrap/generated outputs (or defer theseProgramInput`-typed declarations until that is done).

Useful? React with 👍 / 👎.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 0ac76f8c · Trigger: schedule
• Thinking: 93s wall

---

Findings

• src/v3/compiler/src/test_runner.rs:1854-1864 — decl_inhabits_named_role keys role identity off the literal type-name strings "ProgramInput" / "ProgramOutputBind" looked up via Dag::declaration_by_name. This swaps the old declaration-name sentinel for a type-name sentinel, but the substrate is still doing string dispatch instead of a structural coproduct (per INVARIANTS.md "facts flow forward / single authority"). The two relevant brief comments tracking dissolution (the old PROGRAM_INPUT_SENTINEL block and its sibling lens_decl.name == "named_function_count" block) were trimmed instead of being retitled to track this remaining bridge — there's no longer a named dissolution trigger on the file. NON-BLOCKING but please re-add a short bridge note pointing at the TestPredicate input-coproduct dissolution (per the rule that scaffolds need a documented + bounded + named dissolution trigger).

• src/v3/std/verification.dag:163-170 — ProgramInput and ProgramOutputBind are introduced as free-standing types rather than as variants of an input_ref coproduct on TestPredicate. Today nothing in the type system stops a fixture from passing some unrelated DeclarationRef into LensOutputEquals.input_ref / DifferentialEquals.input_ref — the runner still has to Fail at runtime when neither role is inhabited (e.g. test_runner.rs:1900-1904). Modeling the input slot as a coproduct (type ProgramInputRole = ProgramInput {} | ProgramOutputBind { output_ref: DeclarationRef }, then changing input_ref's static type) would make the illegal state unrepresentable and remove the name-based dispatch above. NON-BLOCKING — a real next step rather than a defect.

Verdict: APPROVE_WITH_COMMENTS. The PR is a real improvement: the per-file cost_bind_for_claim_file table and the declaration-name PROGRAM_INPUT_SENTINEL are gone, replaced by a structural ProgramOutputBind { output_ref } authored in std.verification and consumed via inhabits/meta-tag/instantiation. The remaining bridge is narrower (type-name dispatch) and worth landing now; the two notes above are about finishing the dissolution and keeping the bridge documented, not blocking.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 0ac76f8c · Trigger: schedule
• Thinking: 108s wall

---

Findings

• src/v3/compiler/src/test_runner.rs:1701 collapses ProgramInput and ProgramOutputBind into the same “reflect whole program” path for non-cost_of LensOutputEquals, so ProgramOutputBind.output_ref can be silently ignored. The new schema says ProgramOutputBind selects “one bind” (src/v3/std/verification.dag:167), and the diff adds a live ignored use with named_function_count at src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:175. This violates P2 / modeling discipline “facts flow forward” and “illegal states unrepresentable”: a declared selector fact can be wrong and the claim still passes.

Verdict: REQUEST_CHANGES

The file-name map removal is the right direction, but the new role boundary needs to stay typed: either keep whole-program lenses on ProgramInput, or fail/dispatch separately when ProgramOutputBind appears so output_ref is actually consumed.

[briansrls]

Addressed the blocking feedback and CI failures on the latest branch.

Changes pushed through 45fda180b:

• Split the conflated role shape into ProgramInput {} and ProgramOutputBind { output_ref: DeclarationRef }.
• Regenerated bootstrap snapshots so the new verification roles resolve in fixture compilation.
• Kept the whole-program sentinel only for current named-function-count fixtures because empty record data bodies (ProgramInput = {}) still lower opaque in user fixtures; added a dissolution note in test_runner.rs.
• Made LensOutputEquals fail closed if a non-cost_of lens receives ProgramOutputBind, so output_ref cannot be silently ignored.
• Updated the PR body to reflect the split roles, remaining bridge, and validation.

Validation run locally:

• cargo test -p v3-compiler r1_lane_e_suite -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests test_runner_test -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests t_demo_fixture_test -- --nocapture
• cargo test --workspace --exclude v2-compiler-tests testgen_structural_coverage_gate_test -- --nocapture

[briansrls]

Fixed the CI failures seen on 45fda18 and pushed e742d1442.

Root causes from the v3 log:

• parse_stage4_prep::handwritten_parse_snapshot_matches_manifest needed the parse corpus manifest refreshed for the changed src/v3/std/verification.dag shape.
• t_demo_fixture_test::t_demo_canonical_suites_are_runner_visible still passed ProgramOutputBind to named_function_count, which now correctly fails closed because that lens does not consume an output bind.

Fixes:

• Refreshed src/v3/compiler/tests/integration/parse_corpus_manifest.txt via the ignored refresh test.
• Moved the t_demo named_function_count claim back to the whole-program sentinel and removed the unused upsert_effect/t_demo_effects_program_input focused-bind stub.

Validation:

• cargo test -p v3-compiler handwritten_parse_snapshot_matches_manifest -- --nocapture
• cargo test -p v3-compiler t_demo_canonical_suites_are_runner_visible -- --nocapture

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR moves LensOutputEquals / DifferentialEquals away from a Rust-side filename-to-bind table and toward declared verification roles. The new substrate surface is ProgramInput and ProgramOutputBind in src/v3/std/verification.dag:165 and src/v3/std/verification.dag:169, and the runner now resolves those roles through program_input_role instead of the deleted cost_bind_for_claim_file match. The fixtures then declare per-claim ProgramOutputBind values such as r1_merge_sort_program_input and r1_lane_e_program_input, so cost comparisons select merge_sort_out / lane_e_diff_out from the compiled TestClaim.source program rather than from claim.file_name. The generated bootstrap files are the expected fallout from adding the two verification declarations.

2. Invariant categories

1. LAYER MODEL — Finding, BLOCKING. The diff touches substrate by adding type ProgramOutputBind { output_ref: DeclarationRef } at src/v3/std/verification.dag:169-170, but the implementation admits a state where a ProgramOutputBind selector is accepted and then ignored. The generic LensOutputEquals path treats both ProgramInput and ProgramOutputBind identically via let input_field = if program_input.is_some() { at src/v3/compiler/src/test_runner.rs:1701; the selector is only consumed in the cost_of special case at src/v3/compiler/src/test_runner.rs:1637-1640. The new fixture demonstrates the illegal state: data t_demo_effects_program_input: ProgramOutputBind = { / output_ref: upsert_effect at src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:61-62, then passes that to named_function_count at src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:175, where output_ref has no effect. That makes the new substrate role partly a “whole program input” marker and partly an output selector, with no type-level enforcement of which meaning is live.
2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING. This is the same root issue under illegal states unrepresentable / API-level enforcement: ProgramOutputBind claims to select “one bind in the compiled TestClaim.source program” at src/v3/std/verification.dag:167-170, but the runner accepts it for non-output-selecting lenses because program_input.is_some() is the only gate at src/v3/compiler/src/test_runner.rs:1701. A fixture author can therefore provide a stale or wrong output_ref and still get a passing LensOutputEquals claim for a whole-Dag lens. Fix shape: use ProgramInput for named_function_count / whole-Dag lenses, and either reject ProgramOutputBind unless the predicate/lens actually consumes output_bind_name, or split the role so the output selector cannot be ignored.
3. CODING.md — Compliant. The hand-written runner change mostly follows the data + function style: program_input_role is a small explicit dependency over self.dag and returns Result<Option<ProgramInputRole>, String> with typed branching rather than a global table; see src/v3/compiler/src/test_runner.rs:1814-1851.
4. TESTING.md — Finding, BLOCKING with the substrate fix above. The fixture updates exercise the positive cost-selection path, for example r1_merge_sort_program_input is wired into the merge-sort cost claim at src/v3/compiler/tests/fixtures/r1_gates.dag:195 and the differential claim at src/v3/compiler/tests/fixtures/r1_gates.dag:210. But the same diff also adds a positive example that uses ProgramOutputBind for named_function_count at src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:175, which cements the wrong behavior: the test suite now demonstrates that a selector-bearing role is valid even when the selector is unused. This should be corrected to a ProgramInput fixture or covered by a rejection test.
5. LOCKED DESIGN DECISIONS — N/A. I do not see this diff explicitly altering a locked thesis/design decision; the relevant change is a verification/test-runner role model, not a locked target-lowering or runtime contract.
6. TRACKED vs UNTRACKED DEBT — Finding, NON-BLOCKING once the role misuse is fixed. The PR deletes the old tracked filename bridge, but it still introduces fixture-local name witnesses such as data merge_sort_out: Int = 0 at src/v3/compiler/tests/fixtures/r1_gates.dag:150 solely so output_ref: merge_sort_out can later be converted back into a string bind name at src/v3/compiler/src/test_runner.rs:1842-1850. That may be an acceptable intermediate bridge, but the new ProgramOutputBind docs at src/v3/std/verification.dag:167-170 present it as the steady-state contract rather than naming bounds and a dissolution trigger for replacing fixture-local stub declarations with real references into TestClaim.source.

3. Verdict

REQUEST_CHANGES

The direction is good: the hard-coded filename table is being dissolved into declared verification data. I would not land it as-is because the new ProgramOutputBind role is already used in a case where its output_ref is ignored, which weakens the substrate boundary and normalizes an illegal state in the test fixtures.

[briansrls]

Verified this against current head e742d1442. The finding was valid for reviewed commit 0ac76f8c, but is now addressed.

Current state:

• LensOutputEquals consumes ProgramOutputBind only in the cost_of branch via ProgramInputRole::output_bind_name.
• The generic/non-cost_of path now fails closed if input_ref inhabits ProgramOutputBind, so output_ref cannot be silently ignored.
• The t_demo named_function_count claim no longer uses t_demo_effects_program_input; it uses r1_lens_output_input_from_program instead.
• The unused t_demo_effects_program_input / upsert_effect focused-bind stub was removed.

No additional code change needed for this old-sha review item.

[briansrls]

Review metadata

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

---

Findings

• src/v3/compiler/src/test_runner.rs:1880-1894 — decl_inhabits_named_role resolves ProgramInput/ProgramOutputBind by string lookup (dag.declaration_by_name(role_name)). If the role isn't imported into the merged DAG, the function returns false silently and callers fall through to "input_ref must inhabit ProgramOutputBind". Acceptable for now — it's tagged as a "Narrow bridge" with a named dissolution trigger (input-role coproduct on TestPredicate) — but worth a hard error on dag.declaration_by_name(role_name).is_none() so a future import drop is loud rather than diagnostic-shaped. Non-blocking.

• src/v3/compiler/tests/fixtures/r1_gates.dag:147-159 (and the t_demo and template fixtures) — the fixture-side data merge_sort_out: Int = 0, lane_e_diff_out, complexity_demo_out, total exist purely so ProgramOutputBind.output_ref can carry a DeclarationRef whose name is then used to look up a bind in a different DAG (the compiled claim program). So output_ref is structural in shape but still name-keyed in semantics — the fixture decl's body/type is irrelevant; only its identifier matters. This re-locates the Slice-2 string bridge rather than dissolving it. The PR body and Slice-2 deferral acknowledge this. Non-blocking, but the dissolution trigger comment near cost_bind should probably explicitly call out that output_ref resolution is still string-keyed across DAGs.

Verdict

APPROVE_WITH_COMMENTS — the PR does what the brief promises: splits ProgramInput from ProgramOutputBind, routes cost/differential through structural output_ref, and fails closed when a non-cost_of lens receives ProgramOutputBind. Both remaining bridges (name-keyed role detection and name-keyed bind lookup) are bounded and have named dissolution triggers, satisfying the tracked-debt rule. Generated bootstrap churn is large but mechanical.

[briansrls]

Addressed the non-blocking review notes from e742d144 and pushed 7735f61e9.

Changes:

• decl_inhabits_named_role now fails loudly if the expected verification role type (ProgramInput / ProgramOutputBind) is missing from the fixture DAG, rather than silently returning false.
• Added an explicit cross-DAG bridge note near ProgramOutputBind.output_ref consumption: the fixture-side DeclarationRef still crosses into the compiled TestClaim.source DAG by declaration name, with a dissolution trigger to resolve output-bind identity inside the compiled program DAG.

Validation:

• cargo test --workspace --exclude v2-compiler-tests test_runner_test -- --nocapture

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: e742d144 · Trigger: schedule
• Thinking: 255s wall

---

Verdict: APPROVE

The diff is narrowly scoped: it replaces the hard-coded file-name cost-bind table with fixture-authored ProgramOutputBind role data, keeps the remaining bridge documented with a dissolution trigger, and fail-closes malformed or unused role inputs. No concrete invariant, coding, or testing violation observed.

Checked with:
cargo test -p v3-compiler test_runner_runs_r1_lane_e_suite -- --nocapture
cargo test -p v3-compiler t_demo_canonical_suites_are_runner_visible -- --nocapture

[briansrls]

Review metadata

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

---

1. Story of the diff

This PR replaces a Rust-side, file-name-keyed mapping for structural cost comparisons with a .dag-authored selector. std.verification now declares ProgramInput and ProgramOutputBind, where ProgramOutputBind carries an output_ref: DeclarationRef to name the bind in the compiled TestClaim.source program (src/v3/std/verification.dag:165-171). The runner consumes those roles through program_input_role, fail-closing malformed ProgramOutputBind bodies instead of falling back (src/v3/compiler/src/test_runner.rs:1837-1874), and the R1/t-demo fixtures now point cost and differential predicates at role declarations rather than the old global sentinel/file map (src/v3/compiler/tests/fixtures/r1_gates.dag:155-161, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:50-56). The generated bootstrap fixtures and parse manifest are refreshed to carry the new verification declarations (src/v3/compiler/src/bootstrap_generated.rs:859-860, src/v3/compiler/tests/integration/parse_corpus_manifest.txt:41).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this touches the verification model, not core Dag storage: the new authority is modeled as ProgramOutputBind { output_ref: DeclarationRef } in .dag (src/v3/std/verification.dag:169-170) and consumed by the runner via role parsing (src/v3/compiler/src/test_runner.rs:1837-1843), rather than adding another implementation-only file-name table.

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

Compliant — Boundary Discipline / single authority improves: fixture authors now declare the output bind selector once as data (src/v3/compiler/tests/fixtures/r1_gates.dag:155-157), and malformed selectors fail closed through explicit ClaimResult::Fail paths for missing body, missing output_ref, or non-reference payload (src/v3/compiler/src/test_runner.rs:1844-1863). The remaining name bridge is explicitly bounded by a dissolution trigger: LensOutputEquals.input_ref should become a typed input-role coproduct so the runner receives ProgramInput / ProgramOutputBind directly (src/v3/compiler/src/test_runner.rs:38-42).

1. CODING.md.

Compliant — the PR removes the hard-coded file_name -> bind name helper and replaces it with a small typed carrier, ProgramInputRole, whose output-bind case carries the needed bind name (src/v3/compiler/src/test_runner.rs:1346-1355). The parsing function has a clear Declaration -> Result<Option<ProgramInputRole>, String> shape and keeps every malformed case on an explicit failure path (src/v3/compiler/src/test_runner.rs:1837-1874).

1. TESTING.md.

Finding — NON-BLOCKING: the new rejection path for an output-bind selector passed to a lens that does not consume output binds is not covered by a visible regression claim. The behavior is added at src/v3/compiler/src/test_runner.rs:1712-1718, especially the fail message "input_ref ... inhabits ProgramOutputBind but lens ... does not consume an output bind" at src/v3/compiler/src/test_runner.rs:1717, but the fixture updates only exercise valid ProgramOutputBind uses for cost_of / differential claims (src/v3/compiler/tests/fixtures/r1_gates.dag:194, src/v3/compiler/tests/fixtures/r1_gates.dag:209, src/v3/compiler/tests/fixtures/r1_gates.dag:225, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:94, src/v3/compiler/tests/t_demo/t_demo_fixtures.dag:118). Since this PR includes a fix for rejecting unused ProgramOutputBind inputs, a negative LensOutputEquals claim using ProgramOutputBind with a non-output-bind lens would cement the behavior.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter a locked thesis/design decision; it stays within the existing .dag verification/test-runner bridge and names the remaining dissolution path in code comments.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the temporary shapes are documented and bounded. PROGRAM_INPUT_SENTINEL is retained as a compatibility bridge only until empty-record ProgramInput {} data bodies can be authored (src/v3/compiler/src/test_runner.rs:38-43), and the role-name lookup bridge is explicitly described as narrow, with dissolution tied to the future TestPredicate input-role coproduct (src/v3/compiler/src/test_runner.rs:1877-1881).

3. Verdict

APPROVE_WITH_COMMENTS

No blocking substrate/modeling issue showed up: the PR moves authority out of Rust filename dispatch and into typed .dag declarations, with fail-closed parsing of malformed role values. The one comment is a test gap around the newly added rejection branch, which is implementation/test discipline rather than a reason to block the modeling change.