Lane 1 Stage 1b: substrate keyed-lookup accessors (DB-14)

[briansrls]

Stacked on #495 (Lane 1 Stage 1a). Implements DB-14's substrate-external-primitives pattern (from PR #497's design doc).

What lands

Three substrate accessors — port(d, id) -> DagPort?, node(d, id) -> Behavior?, resolve_producer(d, port_id) -> Behavior? — declared in substrate.dag with trivial { host ... } stubs. Bootstrap upgrades each to ArrowBody::ExternalRealization; emission reads the realization's carrier template and renders per call-site.

Design: docs/design-substrate-external-primitives.md

Pieces

• substrate.dag: SubstrateAccessorRealization, SubstrateAccessorBinding, 3 fn stubs
• rust.dag: 3 realization data records (positional {p0}/{p1} templates) + 3 binding records
• dag.rs: port_opt, node_opt, resolve_producer_opt Option-returning Rust methods
• bootstrap.rs: materialize_substrate_accessors — mirrors materialize_pipeline_realizations; replaces each accessor's Arrow body with ExternalRealization(realization_id) and each realization's Instantiation with the meta's Conj
• infer.rs: signature_type_shape now handles Cardinality, unblocking T? as a callable signature return type (the root cause of the first attempt's "port unresolved" failure)
• emit_rust.rs: render_external_realization dispatch in render_callable_transform
• provenance.dag: migrated — find_port/find_behavior/behavior_id/local carriers deleted (136 → 88 lines)
• unused_parameters.dag: migrated — inputs_for_port_list/inputs_for_node_list/behavior_result_port/behavior_id/ResultPortLookup deleted (185 → 150 lines)
• complexity.dag: unchanged (its lookup_cost walks the lens's own accumulator, not substrate)
• INVARIANTS.md § L-7 + CI grep gate blocking local accessor declarations in src/v3/lenses/*.dag
• Generated modules (lens_provenance_generated.rs, lens_unused_parameters_generated.rs) regenerated

Acceptance

• port / node / resolve_producer declared in substrate.dag as query functions over existing lists; no new parallel fields on Dag
• All three lenses migrated; oracle + snapshot + clone-count ratchet tests pass
• Line reduction ≥15%: 483 → 400 (−17.2%)
• INVARIANTS.md L-7 with grep-gate command
• CI gate blocks fn (find_port|find_behavior|resolve_producer|lookup_node|lookup_port) matches
• Full cargo test -p v3-compiler + cargo clippy --all-targets -- -D warnings green
• banked-dissolutions ratchet: clean

Notes for reviewers

• Carrier template convention: positional {p0}, {p1} placeholders rather than the source-level param names DB-14 initially sketched. Reason: declarations don't carry param-name metadata past lowering, so positional is simpler than round-tripping the source. Convention is opt-in per realization and trivially extensible later.
• The Cardinality fix in infer.rs: when I first tried DagPort? / Behavior? as return types, signature_type_shape returned None for TypeConnective::Cardinality { .. } — the same pattern that walk_to_type_shape handles at line 3048. Added the symmetric case. Unblocks any future substrate fn returning T?.
• The test referenced_port_walk_real_helper_stack_compiles previously re-declared BehaviorLookup inline, which conflicted with substrate's canonical declaration during my first try (carrier-based). The current shape (using T? instead of carriers) doesn't re-introduce the name in substrate, but the test's inline copy is still valid and unchanged.
• Not migrated tonight: go/python emission dispatch for ExternalRealization. Follow-up when those backends are wired (they don't currently emit the lenses; Rust-only is sufficient for today's consumers).

Test plan

• cargo test -p v3-compiler
• cargo clippy -p v3-compiler --all-targets -- -D warnings
• scripts/check-banked-dissolutions.sh
• CI runs the full workspace (this is a draft PR)

🤖 Generated with Claude Code

[briansrls]

codex · gpt-5.4 · 63efcbf1

⚠️ Review (blocking: 2, non-blocking: 2+/0-)

BLOCKING (2)

Root Cause

• docs/design-substrate-external-primitives.md DB-14 models bindings as accessor+realization only even though the design talks about one binding per accessor×target pair -> carry target/language as a typed edge and make bootstrap/emission select exactly one binding for the active target.
• docs/design-substrate-keyed-lookup-api.md DB-5 locks resolve_producer as recursive Bind-chain resolution, but the new carrier/tests only check existence and never distinguish first producer from ultimate producer -> implement the recursive walk and add a bind-hop fixture that proves the contract.

Non-blocking — Strengths

• .github/workflows/ci.yml The L-7 grep gate is the right ratchet: it mechanically blocks new lens-local lookup helpers instead of relying on review memory.
• src/v3/lenses/provenance.dag Switching the lens to substrate port/node accessors removes duplicated lookup logic while still keeping malformed-Dag misses distinct from NoProducer.

⚠️ The substrate accessor direction is good, but the landed pattern still drops per-target selection and resolve_producer's Bind-pass-through contract, so I would fix those before merging.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 63efcbf1d1

ℹ️ 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]

Keep substrate accessors callable on non-Rust targets

Upgrading every substrate accessor to ArrowBody::ExternalRealization here makes port/node/resolve_producer no longer UserDefined, but emit_go and emit_python still only emit ArrowBody::UserDefined functions and have no ExternalRealization render path (see emit_go_with_mode + render_transform, and emit_python_with_mode + render_callable_transform). As a result, any .dag program that uses the newly introduced accessors will compile but generate Go/Python output with unresolved calls (or otherwise unrendered external bodies), so cross-target emission is now broken for that feature.

Useful? React with 👍 / 👎.

[briansrls]

Addressed both blockers (commit 0c07e9a, force-pushed after rebasing onto the updated #495).

1. resolve_producer_opt recurses through Bind hops (dag.rs + substrate test)

Replaced the single-hop implementation with a bounded recursive walk: follow produced_by to the producing Behavior, and if it's a Bind, recurse on bind.value until a non-Bind producer is reached. Bounded by node count; cycles in the Bind chain return None rather than looping. Added resolve_producer_opt_walks_through_bind_hops with a three-level alias chain (base → alias → double_alias) asserting every Bind resolves to a non-Bind. DB-5 contract now satisfied at the substrate → Rust boundary.

2. SubstrateAccessorBinding gets language: DeclarationRef (substrate.dag + rust.dag + bootstrap.rs + emit_rust.rs)

Structural fix — not a validation layer, not a convention, just the missing typed edge.

• substrate.dag: SubstrateAccessorBinding { accessor, realization, language } — language mirrors the language: DeclarationRef edge every other shared realization (TypeRealization, OperatorRealization, …) already uses. Adding a new target = one more data record, zero compiler changes.
• rust.dag: each of the three bindings declares language: rust_language.
• bootstrap.rs: deleted materialize_substrate_accessors. The accessor Arrow bodies stay Unparsed at bootstrap. Target selection moves entirely to emission time — upgrading the body to any single realization at bootstrap is precisely what silently dropped target selection. Pipeline.dag stays unchanged; its stages are target-invariant, which is why the upgrade pattern is correct there and wrong here.
• emit_rust.rs: added RealizationIndexes::substrate_accessors (accessor_decl → realization_decl), built by build_substrate_accessor_index — walks every SubstrateAccessorBinding, filters by language == rust_language, and fails closed with DuplicateRealization on collision (single-authority enforced at the type level). Renamed render_external_realization → render_substrate_accessor; dispatches via the index instead of the Arrow body variant.

Tests: substrate_accessors_exist_in_bootstrap_dag now asserts ArrowBody::Unparsed (with a comment documenting why). substrate_accessor_realization_shape_passes_checks became substrate_accessor_binding_carries_language_selector — verifies every in-tree binding declares language: rust_language.

On the ChatGPT review's framing question ("Rust-only scaffold OR structural target selector"): chose the structural selector. The type now admits exactly one realization per (accessor × language) pair, enforced at emission-index build time. Adding go/python is a pure spec-file change when those emitters land.

Full cargo test -p v3-compiler + clippy + L-7 grep gate + L-8 grep gate (the version updated on #495) + banked-dissolutions ratchet all clean.

🤖 Generated with Claude Code

[briansrls]

@chatgpt-codex-connector the P1 above (commit 63efcbf) is stale — addressed in commit 0c07e9a pushed shortly after. That commit:

• Deletes materialize_substrate_accessors entirely. Accessor Arrow bodies now stay Unparsed at bootstrap (the { host <name> } stub). Upgrading them at bootstrap to one backend's ExternalRealization is exactly the pattern this P1 describes, and it's the root cause; the fix was to remove it rather than add cross-target wiring on top of it.
• Moves target selection to emission time. Each emitter builds its own substrate_accessors: HashMap<accessor_decl, realization_decl> from SubstrateAccessorBinding records filtered by language == <its own LanguageSpec>. See build_substrate_accessor_index in emit_rust.rs. emit_go / emit_python simply don't build this index yet (no Go/Python bindings exist), so they fall through to the existing callable dispatch — no unresolved calls, no broken emission. When those backends land their own bindings, they'll build their own indexes.

Existing test substrate_accessors_exist_in_bootstrap_dag now explicitly asserts ArrowBody::Unparsed (not ExternalRealization) at bootstrap, with a comment documenting why.

Re-review on HEAD (0c07e9a51) welcome.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Keep them coming!

ℹ️ 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".

[briansrls]

Meta-Review (Loop Health)

According to a document from 2026-04-17, this loop is still making real progress. It is not just churning. But it is one narrow round away from flipping from productive iteration into debt-shifting if the contract drift is not closed now. chatgpt-review-21600125-7d0a-46…

Loop summary.

Visible history shows 3 review rounds over at least 2 reviewed code states; the exact Git commit count is not exposed by the attachments, so I’m not going to invent it. The logged review mix is 1 codex-cli review and 2 chatgpt-browser reviews, spanning roughly 8 hours 15 minutes from the first browser review at 05:31Z to the second browser review at 13:46Z on 2026-04-17. chatgpt-review-21600125-7d0a-46…

Forward progress evidence.

This PR did enable real consumers. The substrate keyed-lookup accessors are not sitting unused: provenance.dag and unused_parameters.dag were migrated to consume port(...), node(...), and resolve_producer(...) instead of maintaining lens-local list walks, and the generated Rust surfaces dropped the old lens-local lookup coproducts. That is principle-1 progress: new substrate facts are actually being consumed by real downstream paths, not just declared. chatgpt-review-21600125-7d0a-46…

chatgpt-review-21600125-7d0a-46…

The loop also retired earlier blockers instead of rediscovering them. The first round’s substrate-shape complaint was that SubstrateAccessorBinding lacked a target dimension and therefore allowed multiple realizations with no canonical active target; the later round explicitly records that this was fixed by adding language and rejecting duplicate accessor×language bindings. Likewise, codex flagged resolve_producer because the carrier/tests did not prove Bind-chain pass-through; the later browser review says that issue is fixed too, with recursive Bind walking and a regression test pinning it. That is genuine review-loop payoff. chatgpt-review-21600125-7d0a-46…

chatgpt-review-21600125-7d0a-46…

The loop also graduated one recurring pattern into a structural ratchet: the new L-7 CI gate blocks new lens-local lookup helpers, replacing “remember not to do that again” with mechanical enforcement. That is exactly the kind of invariant graduation the discipline calls for, and it materially improves the loop’s health. chatgpt-review-21600125-7d0a-46…

chatgpt-review-e7bbccb3-10ca-42…

Debt accumulation evidence.

There is still debt accumulation, but it is localized rather than diffuse. First, the loop added net-new scaffold surface around substrate accessors. The project’s own invariant is that scaffolds are acceptable only with bounded triggers and explicit gates; otherwise they are just delayed substrate debt. The accessor work is not debt-free just because it is moving in the right direction. chatgpt-review-e7bbccb3-10ca-42…

Second, the loop has not yet made the target-accessor contract singular. The later browser review says the implementation and tests now commit to “accessor bodies stay Unparsed; target selection happens at emission time via SubstrateAccessorBinding,” while DB-14 and nearby comments still describe the rejected bootstrap-upgrade-to-ExternalRealization model. That is not a minor doc nit. It is a parallel authority. The invariants explicitly call this out: if the design doc claims a substrate shape, it must name the actual substrate target, or the implementation will drift into synthesized or parallel representations. Right now, the loop has one code contract and one prose contract. chatgpt-review-21600125-7d0a-46…

chatgpt-review-e7bbccb3-10ca-42…

Third, the remaining behavioral gap is still fail-open. The same later review says the active-target coverage invariant is convention-level because a declared substrate accessor can still have no binding for the active emitter and the miss path just falls through. That is still debt, and it is substrate-level debt, which the modeling discipline treats as blocking because it propagates quickly once copied. chatgpt-review-21600125-7d0a-46…

chatgpt-review-e53a09c4-8361-45…

Cheating signal.

Mostly honest. The good sign is that this codebase is at least documenting scaffolds as scaffolds: the current invariant set requires explicit 🟡 SCAFFOLD ... dissolves when ... triggers for temporary realization shapes, and this loop is operating in that culture rather than hiding every compromise behind “TODO later.” That lowers the cheating signal. chatgpt-review-e7bbccb3-10ca-42…

chatgpt-review-e7bbccb3-10ca-42…

But the loop is not fully clean here. The most important remaining compromise — the split between the code/test contract and the DB-14/source-comment contract, plus the fail-open “no binding for active target” miss path — is not yet surfaced as a bounded scaffold with a singular receipt. It is just present. That is the kind of “good enough for now” compromise that becomes expensive if one more consumer copies it. So the implementer is not hiding everything, but the last unresolved issue is still being carried more quietly than it should be. chatgpt-review-21600125-7d0a-46…

chatgpt-review-e7bbccb3-10ca-42…

Meta-verdict — 📈 KEEP_ITERATING

This is not a stagnant loop. It has already paid off prior findings with structural fixes, real consumer migration, and a new ratchet. Calling pause now would be wrong. Shipping now would also be wrong, because the remaining issue is substrate-level and still fail-open. The right call is one more tight round whose entire job is to do two things:

1. Make DB-14, substrate comments, code, and tests name one target-accessor contract.
2. Make “declared accessor but no realization for the active target” a hard error, not a fallthrough.

If the next round does anything broader than that, the loop starts shifting debt. If it closes those two points, this will have been a healthy loop, not a bluff.

---

View conversation

[briansrls]

codex · gpt-5.4 · 0c07e9a5

✅ Review (blocking: 0, non-blocking: 2+/1-)

Non-blocking — Strengths

• src/v3/compiler/src/emit_rust.rs build_substrate_accessor_index keeps target selection structural and single-authority by filtering on language == rust_language and failing closed on duplicates.
• .github/workflows/ci.yml The L-7 grep gate is the right ratchet: future lenses now have to consume substrate accessors instead of reintroducing local lookup scaffolding.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/design-substrate-external-primitives.md DB-14 still describes the superseded bootstrap ArrowBody::ExternalRealization upgrade path even though HEAD leaves accessor bodies Unparsed and does language-filtered binding selection at emission time; update the authority doc before Lane 1e builds on it.

✅ The substantive blockers are fixed and the landed accessor path now matches the thesis on single authority, facts flowing forward, and fail-closed target selection.

[briansrls]

Addressed ChatGPT's round-1b.4 review (commits b8093de + 9be4671).

BLOCKING — fail-closed on missing active-target realization (emit_rust.rs + test)

render_substrate_accessor now distinguishes three cases at the miss path:

1. Template is in substrate_accessors (per-target map) → render the realization's carrier.
2. Template is in substrate_accessor_universe (declared accessor, but no binding for THIS target) → EmitError::UnsupportedBehavior with a specific fix message pointing at the missing binding. No more silent fall-through.
3. Template is NOT in the universe (ordinary callable) → Ok(None) so normal dispatch handles it.

Structural, not a check: substrate_accessor_universe: HashSet<DeclarationId> is built from every SubstrateAccessorBinding record across ALL languages (not filtered). build_substrate_accessor_index now returns (per_target_map, universe) as a tuple so the two sets stay derived from the same walk.

Coverage invariant pinned by substrate_accessor_universe_fully_covered_for_rust — asserts every accessor in the universe has a rust_language binding today. If someone adds a go-only accessor in the future without a Rust counterpart, that test flags the gap before emit_rust errors at a random call site.

NON-BLOCKING — DB-14 doc drift (docs/design-substrate-external-primitives.md + inline source comments)

Rewrote the authority doc to match the landed design instead of the superseded bootstrap-upgrade path. Highlights:

• TL;DR describes two dispatch patterns: pipeline.dag (target-invariant, bootstrap-upgrade) vs. substrate.dag (target-variant, emission-time binding index) — and why they diverge.
• §4 shows the SubstrateAccessorBinding { accessor, realization, language } shape with the required language selector.
• §5 retitled "Bootstrap: NO upgrade for substrate accessors" with explicit rationale. Pipeline.dag's bootstrap-upgrade stays untouched; substrate accessors need per-target dispatch so the upgrade pattern is rejected here.
• §6 describes the emission-time index + universe + fail-closed coverage check.
• Acceptance list converted from [ ] to [x] with line-count numbers (lens reduction 483→400, −17.2%) and test names.
• Status flipped to "Landed on PR Lane 1 Stage 1b: substrate keyed-lookup accessors (DB-14) #501."

Also refreshed the inline comments in substrate.dag and rust.dag that described the old story.

Ratchet still clean: v3 tests, clippy, banked-dissolutions, L-7 gate.

Re-review on HEAD (9be4671d6) welcome.

🤖 Generated with Claude Code

[briansrls]

ChatGPT Review

Principle audit.

Fail-closed. Mostly satisfied, and the previously raised fail-closed gap looks fixed: duplicate (accessor × language) bindings now error, malformed binding/realization shapes error, and “bound in some target but missing for Rust” is no longer a silent fallthrough. My one remaining BLOCKING concern is the zero-binding case. DB-14 says emission should fail closed when a substrate accessor is declared but has no binding for the active target (docs/design-substrate-external-primitives.md:78-85), but emit_rust only puts accessors into substrate_accessor_universe if they already appear in some SubstrateAccessorBinding record (src/v3/compiler/src/emit_rust.rs:530-540, 851-855, 892-893). If a new accessor is declared in src/v3/std/substrate.dag but no binding is added anywhere, render_substrate_accessor treats it as “not a substrate accessor at all” and falls through (src/v3/compiler/src/emit_rust.rs:3446-3466). The current test also locks only the binding-derived universe, not declaration coverage (src/v3/compiler/tests/m1_substrate_test.rs:2892-2945).

Illegal states unrepresentable. The earlier illegal-state blocker is fixed: SubstrateAccessorBinding now carries language, and duplicate (accessor × language) pairs are rejected (src/v3/std/substrate.dag:265-280; src/v3/compiler/src/emit_rust.rs:857-907). The remaining hole is the same zero-binding state: std/substrate.dag can declare a substrate accessor (src/v3/std/substrate.dag:238-293) without any structural fact tying that declaration into the binding universe, so “declared accessor, zero bindings anywhere” is still representable.

Facts flow forward. Satisfied. This round really does move the keyed-lookup fact to its origin and consume it downstream: provenance and unused-parameters now read port/node instead of rebuilding local list walks (src/v3/lenses/provenance.dag:32-76; src/v3/lenses/unused_parameters.dag:7-133), the generated Rust snapshots shrink accordingly (src/v3/compiler/src/lens_provenance_generated.rs:11-32; src/v3/compiler/src/lens_unused_parameters_generated.rs:8-173), and inference now preserves Cardinality-typed accessor returns instead of dropping them at the signature boundary (src/v3/compiler/src/infer.rs:3086-3090).

Coproduct dissolution. Satisfied. No new substrate enum was added, and the two new substrate records are explicitly tracked scaffolds with a named Lane 1e dissolution trigger (src/v3/std/substrate.dag:254-280). That’s the right shape here.

Single authority. This is where the remaining concern bites deepest. src/v3/std/substrate.dag is the natural authority for “which declarations are substrate accessors” (src/v3/std/substrate.dag:238-293), but emit_rust currently derives the accessor universe from binding data instead (src/v3/compiler/src/emit_rust.rs:530-540, 851-855, 892-893). That splits one fact across two partial authorities: declarations define the accessors, bindings define only the subset somebody remembered to bind.

API-level enforcement. Improved, but not complete. The L-7 grep ratchet is excellent (INVARIANTS.md:2269-2304; .github/workflows/ci.yml:107-118), and duplicate target bindings are mechanically blocked. But nothing in the API stops a contributor from adding fn foo(...){ host foo } to std/substrate.dag and forgetting every SubstrateAccessorBinding; the emitter will not mechanically know that foo was supposed to be part of the fail-closed substrate-accessor set.

Design question. What is the canonical authority for the substrate-accessor set: the declarations in std/substrate.dag, or the per-target binding records? Right now DB-14’s prose and the declaration site read like the first, while emit_rust implements the second. What’s at stake is whether “declared accessor with no realization” is structurally impossible, as the thesis/modeling-discipline want, or still a convention the next accessor author has to remember by hand.

Verdict. REQUEST_CHANGES. The earlier blockers look fixed, the lens migration is real progress, and the new L-7 ratchet is exactly the kind of mechanical guard this lane needed. I would close the remaining substrate-level authority gap before merge by making the accessor universe derive from declarations, or by adding an equally hard ratchet that every declared substrate accessor is bound at least once.

LOOP HEALTH: converging — this round fixes the earlier blockers, migrates real consumers, and adds a useful ratchet; the remaining issue is one narrower substrate-shape gap, not a spread of new debt.

---

View conversation

[briansrls]

ChatGPT Review

Principle audit.

Fail-closed. Improved a lot. The prior active-target miss is now closed the right way: duplicate (accessor × language) bindings error in the index build, and render_substrate_accessor errors instead of silently falling through when Rust lacks a binding (src/v3/compiler/src/emit_rust.rs:859-879, 3453-3474). My remaining BLOCKING concern is one level earlier: substrate_accessor_universe is populated only from existing binding records, and DB-14 locks the same rule (docs/design-substrate-external-primitives.md:166-184, 242). So if someone declares a fourth substrate accessor but forgets to add any binding at all, the emitter will classify it as “not a substrate accessor” and fall through to generic callable rendering rather than failing closed. The current protection is behavioral, not structural: the test only checks the current binding-derived universe and hardcodes the current binding count (src/v3/compiler/tests/m1_substrate_test.rs:2892-2999).

Illegal states unrepresentable. Same BLOCKING issue. The model still admits “declared substrate accessor, zero bindings anywhere,” even though that should be impossible once the accessor is public and callable. Nothing in SubstrateAccessorBinding or the emitter API makes that state unrepresentable; the only backstop is the current manual test expecting three bindings (src/v3/compiler/tests/m1_substrate_test.rs:2997-2999). On the positive side, adding language to SubstrateAccessorBinding is the right fix for the earlier overwrite bug, and signature_type_shape now preserves Cardinality-typed signatures instead of dropping optional-return accessors (src/v3/compiler/src/infer.rs:3090).

Facts flow forward. Mostly satisfied. The lookup fact now originates once in src/v3/std/substrate.dag, is realized in src/v3/spec/rust.dag, and the migrated lenses consume those declarations instead of rebuilding local scans (src/v3/std/substrate.dag:261-291; src/v3/lenses/provenance.dag:68-74; src/v3/lenses/unused_parameters.dag:101-131). The one fact that still drops is accessor identity itself: emission re-derives “is this a substrate accessor?” from binding presence rather than carrying that fact forward from the declaration. That is the root of the blocker above.

Coproduct dissolution. Satisfied. No new substrate enum lands here, and the PR goes the right direction by deleting the lens-local lookup coproducts from both the .dag sources and the generated Rust. This is real dissolution, not a rename.

Single-authority metadata. Mostly satisfied, with one structural split remaining. Centralizing the actual lookup operations in std/substrate.dag is exactly the right authority move, and the new L-7 ratchet is a useful guardrail (INVARIANTS.md:2269+; .github/workflows/ci.yml:107-119). The remaining split is that “this declaration is a substrate accessor” is not declaration-owned at emission time; it is inferred from whether some binding happens to mention it. That leaves the declaration and the binding table as competing authorities for one fact.

API-level enforcement. Improved, but still behavioral at the critical point. The Rust-side tests are good, and the CI grep gate is worthwhile, but they do not make the zero-binding state impossible to construct. Right now the enforcement story is “remember to add the binding and keep the hardcoded count test updated,” not “the type/API forces total coverage.” For a substrate-level path, I think that is still too soft.

Design question. What is the canonical authority for “this Arrow is a substrate accessor” — the declaration itself, or the existence of at least one SubstrateAccessorBinding record? Right now DB-14 answers that from the binding side table, but the semantic fact is born on the declaration side. If that stays split, the next accessor addition can reopen the exact fail-open class this PR is trying to close: one missed binding anywhere and emission quietly treats a real substrate primitive as an ordinary callable. The thesis wants the spec to be the implementation and below-boundary facts to move structurally, not by optional side tables, and the review discipline is explicit that substrate-shape leaks are the ones to stop now, not later. chatgpt-review-9ed99a8c-7195-4c…

chatgpt-review-24161f71-5de7-4f…

Verdict. REQUEST_CHANGES. The PR makes real progress: the migrated lenses are cleaner, the old missing-Rust-binding fail-open is genuinely fixed for the current three accessors, and the CI/test ratchets are meaningful. But I would not bank DB-14 yet while “declared accessor with zero bindings” is still representable and still falls through.

LOOP HEALTH: converging — this round deletes real local scaffolding, lands actual consumers and ratchets, and fixes the prior blocker, but the declaration-vs-binding authority split should be closed before the next accessor or backend lands.

---

View conversation

[briansrls]

codex · gpt-5.4 · 76a04bda

⚠️ Review (blocking: 1, non-blocking: 1+/1-)

BLOCKING (1)

Root Cause

• docs/design-m2-feature-parity.md DB-11 has not decided how a where-predicate stops being tied to one function's parameter binding before it is shared as a declaration-level fact; either keep refined declarations site-local or define an alpha-normalized predicate carrier before sharing them.

Non-blocking — Strengths

• src/v3/std/substrate.dag The new SubstrateAccessorRealization and SubstrateAccessorBinding records carry explicit yellow scaffold receipts with a named Lane 1e dissolution trigger, so this substrate extension is tracked debt rather than open-ended scaffolding.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/lane1-stage-b-substrate-keyed-lookup.md This still reads as the pre-landing plan (Status: Plan, unchecked acceptance gates, .dag-body sketches), so update it or mark it historical in the next Lane 1 docs-cleanup pass.

ROADMAP — Incomplete

• DB numbering cleanup: docs/post-l15-phase-plan.md still documents the temporary DB-10..DB-14 numbering collision as follow-up work rather than a settled authority.

⚠️ The stage-1b implementation itself looks clean, but the mixed PR still adds a DB-11 authority doc with one unresolved binder-identity decision that should be locked before implementers treat it as ground truth.

[briansrls]

BLOCKING: DB-11 says two functions can share the same refined declaration even though the refinement predicate is lowered against a parameter-scoped port, so the design currently puts a function-local fact on a globally shared type edge without specifying binder normalization (single authority / illegal states unrepresentable).

[briansrls]

codex · gpt-5.4 · 76a04bda

⚠️ Review (blocking: 1, non-blocking: 1+/1-)

BLOCKING (1)

Root Cause

• docs/design-m2-feature-parity.md DB-11 has not decided how a where-predicate stops being tied to one function's parameter binding before it is shared as a declaration-level fact; either keep refined declarations site-local or define an alpha-normalized predicate carrier before sharing them.

Non-blocking — Strengths

• src/v3/std/substrate.dag The new SubstrateAccessorRealization and SubstrateAccessorBinding records carry explicit yellow scaffold receipts with a named Lane 1e dissolution trigger, so this substrate extension is tracked debt rather than open-ended scaffolding.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/lane1-stage-b-substrate-keyed-lookup.md This still reads as the pre-landing plan (Status: Plan, unchecked acceptance gates, .dag-body sketches), so update it or mark it historical in the next Lane 1 docs-cleanup pass.

ROADMAP — Incomplete

• DB numbering cleanup: docs/post-l15-phase-plan.md still documents the temporary DB-10..DB-14 numbering collision as follow-up work rather than a settled authority.

⚠️ The stage-1b implementation itself looks clean, but the mixed PR still adds a DB-11 authority doc with one unresolved binder-identity decision that should be locked before implementers treat it as ground truth.

[briansrls]

Addressed both NON-BLOCKING items from the latest ChatGPT review (commit 10a6b42 + pre-push fmt).

Fixed m1_5_testgen_test.rs:233-239 drift — the inline match panicked on MissingCost but passed a raw i64 (possibly negative) to compare_cost. The other three consumers already validate sign. Now routes through the new shared helper require_fixture_cost_i64 so both invariant violations panic with specific fixture-context messages.

Removed the duplicated interpretation — the "fixture cost must be FoundCost and non-negative" rule now lives once in tests/common/mod.rs:

• require_fixture_cost_i64(lookup, context) -> i64 — for callers that want i64 (e.g. m1_5_testgen's comparison ops, which take i64 × i64 → bool).
• require_fixture_cost_usize(lookup, context) -> usize — for the majority (indexing, arithmetic as usize).

Both share one sign-check and one MissingCost message. Callers supply a context string so test-failure output names the specific bind/port/fixture.

Migrated:

• m1_3_lens_cost_test::expect_cost → require_fixture_cost_usize.
• thesis_validation_test::bind_cost → require_fixture_cost_usize.
• m1_5_testgen_test's cost-bounded branch → require_fixture_cost_i64.

Intentionally not migrated: src/v3/compiler/src/lens_testgen::bind_cost_of. It's production code (src/) that can't import from tests/common/ — the Rust module graph rules it out. It treats "bind not found" as Option::None (legitimate testgen skip) rather than panic, which is an API-shape difference, not an interpretation difference. The two panic cases it handles (MissingCost, negative-cost) mirror the shared helpers verbatim; comments in both spots cross-reference so drift is visible at review.

Also rebased onto main after #495 merged. Clean cherry-pick of the four 1b-only commits (DB-14 doc + 1b core + round 1b.3 fix + round 1b.4 fix) plus this fix on top, zero conflicts with main.

Full cargo test -p v3-compiler + clippy clean.

🤖 Generated with Claude Code

[briansrls]

ChatGPT review in progress... (view conversation)

Check back in ~30 minutes for the full review.

[briansrls]

Quick triage on the latest round:

Codex BLOCKING (on docs/design-m2-feature-parity.md:102, DB-11 binder identity) — this file is not in this PR's diff. It's the DB-10..DB-13 design doc that landed on main via PR #494 (commit 3df2451); my diff vs main is 18 files, none of them design-m2-feature-parity.md. Codex is flagging content that's already on main, surfaced because the review tool sees the merged tree state. The DB-11 binder-normalization question is a real Lane 3 design concern and deserves its own follow-up PR against #494's doc, not a block on 1b substrate accessors. Marking this blocker as out-of-scope for #501.

Codex NON-BLOCKING: "docs/lane1-stage-b-substrate-keyed-lookup.md still reads as pre-landing plan" — fair catch. Updated the Status line from "Plan. No code changes yet." to "Landed on PR #501 (shipped with R1/R2 shape; docs/design-substrate-external-primitives.md is now at R3 and the convergence will land in a follow-up)." Rolled into the trigger-ci commit (now 4e4b785).

ROADMAP item: DB numbering collision — separate cleanup PR territory; touching it here would expand scope for a mechanical renumber that's better done in one sweep across all affected docs.

ChatGPT review pending on 23e9ef0 — will address if it surfaces anything new on the current HEAD.

CI running now (first time on this branch — earlier pushes didn't trigger; the empty trigger-ci commit did). Will merge once it's green.

🤖 Generated with Claude Code