Skip to content

fix(r3): type UserDefined arrow body bind witness - #1548

Merged
briansrls merged 13 commits into
mainfrom
codex/r3-arrow-userdefined-bindref
May 3, 2026
Merged

briansrls merged 13 commits into
mainfrom
codex/r3-arrow-userdefined-bindref

Conversation

@briansrls

@briansrls briansrls commented May 3, 2026 •

Copy link
Copy Markdown
Contributor

Summary

  • add BindNodeId as the typed witness for ArrowBody::UserDefined
  • change ArrowBody::UserDefined from raw NodeId to BindNodeId
  • convert emitter, lens, inference, lowering, and test consumers to read the bind through the witness instead of re-checking the raw node invariant
  • update bootstrap generation so generated snapshots emit BindNodeId::new(NodeId(...))

Debt receipt

  • Debt paid: docs/debt/r3-debt-paydown-ledger-2026-05-02.md row Emitter as_bind().expect() panic paths; substrate side retires the state-space leak by making ArrowBody::UserDefined carry a typed bind witness. PB can now mechanically sweep the target-private emitter residuals without encoding the invariant per consumer.
  • Debt found + routed: none.
  • No debt touched: not applicable; this PR directly pays the substrate portion of the cited row.

Validation

  • cargo check -p v3-compiler
  • cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify
  • cargo test -p v3-compiler --test integration m1_substrate_test::m17_brace_bodied_fn_parses_single_expr_to_user_defined_arrow_body -- --exact
  • cargo test -p v3-compiler --test integration m1_substrate_test::prereq3_annotated_lambda_direct_call_uses_declared_params_only -- --exact
  • cargo test -p v3-compiler --test integration m2_feature_parity_test::test_db11_type_alias_refinement_predicate_bind_tags_alias_subject -- --exact
  • cargo fmt --all --check
  • git diff --check

@briansrls briansrls changed the title R3 Substrate fix(r3): type UserDefined arrow body bind witness May 3, 2026
@briansrls
briansrls marked this pull request as ready for review May 3, 2026 00:15
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 276d6e1b · Trigger: schedule
  • Comparison: origin/main @ 3c77a60c ... review/pr-1548-276d6e1b @ 276d6e1b
  • Thinking: 28s wall

Verdict: APPROVE — clean, narrowly-scoped refactor.

The PR introduces a typed witness BindNodeId wrapping NodeId for ArrowBody::UserDefined, replacing ~7 sites of repeated dag.node(*id).as_bind().expect(...) revalidation with a single bind(dag) accessor. This is exactly the "illegal states unrepresentable / single authority" pattern from docs/modeling-discipline.md applied to substrate: the invariant ("UserDefined points at a Bind") is now stated once at the type level, and consumers stop re-asserting it.

All construction sites (lower.rs 4 spots, infer.rs materialize_substituted_refined_decl, regen emitter, bootstrap_generated) are updated consistently. The witness is constructed only after the corresponding BindNode is created in the same function, so BindNodeId::new being unvalidated pub(crate) is fine — it's the bootstrap-assertion-at-the-edge pattern.

Minor observations (non-blocking):

  • rust_target.rs:2500 previously returned EmitError::MalformedUserDefinedCallable { detail: "...does not point to a Bind node" }; that error path is now an expect-panic inside BindNodeId::bind. That's the right move (the witness makes the error unreachable), but if you want to be paranoid the panic message could mention which declaration was malformed.
  • dag.rs:1370 Some((*bind_id).bind(dag)) — fine, just slightly awkward; Some(bind_id.bind(dag)) reads the same since BindNodeId: Copy.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 276d6e1b · Trigger: schedule
  • Thinking: 171s wall

BLOCKING (1)

Root Cause

  • src/v3/compiler/src/dag.rs raw NodeId allocation remains separate from the typed bind witness → mint BindNodeId only through a Dag API that creates or validates a Behavior::Bind, or return a diagnostic-bearing checked result instead of an unchecked witness.

⚠️ The direction is good, but the new substrate witness needs to be enforced at construction rather than asserted later.

Comment thread src/v3/compiler/src/dag.rs Outdated
pub struct BindNodeId(NodeId);

impl BindNodeId {
pub(crate) fn new(id: NodeId) -> Self {

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 759eace7 · Trigger: schedule
  • Comparison: origin/main @ 3c77a60c ... review/pr-1548-759eace7 @ 759eace7
  • Thinking: 68s wall

Findings

  • src/v3/compiler/src/emit/rust_target.rs:2503 (P3 fail-closed / CODING.md “hidden panic surface”) — In analyze_user_defined_callable, the diff replaces a branch that returned EmitError::MalformedUserDefinedCallable { detail: "user-defined callable body does not point to a Bind node", .. } when as_bind() was None with let bind = (*bind_id).bind(dag);, which panics on the same condition. That removes a typed, caller-visible emission failure in favor of a contract expect, which is a small regression against the documented preference for structured errors at boundaries.

Note: The same “as_bind()? / continue → .bind() panic” tightening appears elsewhere in the diff (e.g. infer.rs callable_signature_context, resolve_lambda_parameter_types, validate_user_defined_function_signatures, dag.rs declaration_body_bind, lower.rs outer_predicate_slots). Those are mostly internal consistency assumptions; the rust emit path is the one that dropped an existing EmitError variant.

Verdict

APPROVE_WITH_COMMENTS — Introducing BindNodeId and threading it through lowering, inference, lenses, and regen is aligned with boundary discipline / typed witnesses (comments in dag.rs spell that out). No issues with the mechanical bootstrap/regen or manifest updates. The only substantive concern is preserving typed MalformedUserDefinedCallable (or an equivalent Result-shaped check) on the emit boundary instead of panicking when the arrow body is not a bind.

Exploratory (optional)

  • BindNodeId::new is unchecked — the invariant is still behavioral (documented + .bind() panics), not type-enforced at construction. That matches how similar witnesses are often introduced; a future step could add a fallible constructor used at lowering time if you want API-level enforcement without widening pub surface.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head ffba1ca38: this blocking finding was valid on reviewed commit 276d6e1b and is now addressed. BindNodeId::new is gone; external construction uses BindNodeId::from_bind_node(dag, id), which checks dag.node_opt(&id).and_then(Behavior::as_bind) before returning the witness. The only unchecked constructor is private to dag.rs and used by generated bootstrap code inside the module boundary. Lowering/inference construction sites now call the checked constructor after pushing Behavior::Bind.\n\n— sent from jolly-ram-908

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 9ee8bcb2 · Trigger: schedule
  • Comparison: origin/main @ 3c77a60c ... review/pr-1548-9ee8bcb2 @ 9ee8bcb2
  • Thinking: 80s wall

Verdict: APPROVE

The diff makes ArrowBody::UserDefined carry a BindNodeId witness instead of a raw NodeId, which tightens the substrate boundary and removes repeated consumer-side as_bind() checks. I did not see concrete violations of the pinned invariants, coding discipline, or test discipline in the changed lines. No builds or tests run, per review instructions.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 9ee8bcb2 · Trigger: schedule
  • Thinking: 178s wall

✅ This is a focused substrate tightening that carries the bind witness forward to downstream consumers without introducing a new competing authority.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 30573de4 · Trigger: schedule
  • Comparison: origin/main @ d2e72d26 ... review/pr-1548-30573de4 @ 30573de4
  • Thinking: 52s wall

Verdict: APPROVE — clean, narrowly scoped refactor.

The change introduces a typed witness BindNodeId so that ArrowBody::UserDefined carries "this is a Bind" structurally rather than re-deriving it at every consumer with as_bind().expect(...). That's straightforwardly aligned with modeling discipline (illegal states unrepresentable, facts flow forward — validate once at construction, downstream readers consume the witness).

Mechanics check out:

  • from_bind_node is the validating constructor; new_unchecked is private (fn, not pub) and only reachable from dag's child modules (bootstrap_generated*) plus the regen emitter that produces them — exactly the right encapsulation. External call sites in lower.rs and infer.rs (e.g. lower.rs:578, lower.rs:1326, lower.rs:4643, lower.rs:4803, lower.rs:5127, infer.rs:3768) all go through from_bind_node(...).expect(...), which preserves the existing R13-era invariant.
  • All consumers (emit.rs:1473/2162/2206, lens_apply.rs:141/199/272/653, infer.rs:1194/1765/2252/3049/3105, dag.rs:1377) collapse to (*id).bind(dag). The single remaining expect lives inside BindNodeId::bind, which is the desired chokepoint.
  • regen_bootstrap_emit.rs correctly emits BindNodeId::new_unchecked(NodeId(...)), matching what bootstrap_generated.rs now contains.

No findings.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 30573de4 · Trigger: schedule
  • Thinking: 308s wall

BLOCKING (1)

Root Cause

  • src/v3/std/substrate.dag ArrowBody's .dag payload model was not advanced with the Rust witness → declare the bind witness in the substrate model and regenerate consumers so .dag remains the meta-language authority.

⚠️ One substrate authority mismatch remains.

/// User-defined function. BindNodeId is the root bind of a sub-DAG of L1
/// behavior nodes in `Dag.nodes`. Inference walks the sub-DAG and checks
/// the body against the declared inputs/output.
UserDefined(BindNodeId),

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: f805a74a · Trigger: schedule
  • Comparison: origin/main @ d2e72d26 ... review/pr-1548-f805a74a @ f805a74a
  • Thinking: 47s wall

Findings

None. The diff aligns ArrowBody::UserDefined with a real substrate witness (BindNodeId in substrate.dag and a Rust newtype in dag.rs), wires construction through BindNodeId::from_bind_node, and updates emit/infer/lens/lower call sites so consumers use bind / bind_opt instead of repeating as_bind() checks — consistent with docs/modeling-discipline.md Practice 2 (illegal states unrepresentable) and Practice 6 (API-level enforcement). infer.rs decide_transform no longer falls back to t.output when a claimed bind edge was wrong (unwrap_or(t.output)); that was masking inconsistency rather than fail-closed user diagnostics, so tightening it matches the new witness story.

Verdict

APPROVE — The change is coherent end-to-end (DAG declaration, bootstrap emission, regen). Large bootstrap_generated*.rs churn is proportionate to the stored shape change. No concrete violation of the cited rubric surfaced in the substantive diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the blocking substrate mismatch against 30573de4: the finding was valid. Rust had advanced ArrowBody::UserDefined to BindNodeId, while src/v3/std/substrate.dag still declared UserDefined(NodeId).

Addressed on current head a051996489:

  • src/v3/std/substrate.dag now declares substrate type BindNodeId { node: NodeId }.
  • ArrowBody::UserDefined now carries BindNodeId in the substrate authority.
  • Regenerated bootstrap_generated.rs and bootstrap_generated_without_parse_surface.rs; generated snapshots now include the BindNodeId declaration and still emit Rust ArrowBody::UserDefined(BindNodeId::new_unchecked(...)) for checked-in bootstrap rows.
  • Refreshed parse_corpus_manifest.txt for the substrate.dag change.

Validation run:

CARGO_TARGET_DIR=/tmp/gunbc-1548-fix-target RUSTC_WRAPPER= cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify
cargo fmt --all --check
git diff --check

All passed.

— sent from jolly-ram-908

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: a0519964 · Trigger: schedule
  • Comparison: origin/main @ d2e72d26 ... review/pr-1548-a0519964 @ a0519964
  • Thinking: 73s wall

Verdict: APPROVE

Diff is narrowly scoped around replacing raw NodeId arrow bodies with BindNodeId witnesses, plus regenerated bootstrap updates and test call-site cleanup. I don’t see a concrete violation of the pinned invariants, modeling discipline, coding guidance, or testing guidance in the changed lines. Tests/builds were not run per instruction.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: 9fd466c2 · Trigger: schedule
  • Comparison: origin/main @ 58b52651 ... review/pr-1548-9fd466c2 @ 9fd466c2
  • Thinking: 38s wall

Findings

None. The diff aligns P2 (boundary discipline) and modeling “illegal states unrepresentable”: ArrowBody::UserDefined is no longer a raw NodeId in both substrate.dag and dag.rs; it carries a BindNodeId witness, with validation at construction (from_bind_node) and stable access (bind / bind_opt). That removes repeated as_bind().expect(...) at emitters, inference, lowering, and lens apply, and fixes the old decide_transform path that could fall back to t.output when as_bind() was None (infer.rs around the removed unwrap_or(t.output)), which was weaker than “UserDefined means bind body.”

BindNodeId::bind still uses expect internally (dag.rs — same panic-on-contract-violation pattern as the removed expects; CODING.md already treats existing code as debt). No new string-sentinel or duplicate authority issue stands out in the hand-written diff.

Large churn in bootstrap_generated*.rs matches substrate line shifts + declaration id bump from the .dag edit; expected for this repo.

Verdict

APPROVE — Scope is tight: substrate + Rust mirror + mechanical consumer updates + regen/manifest/tests. No concrete rubric violation in the diff reviewed.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 9fd466c2 · Trigger: schedule
  • Thinking: 307s wall

BLOCKING (1)

Root Cause

  • src/v3/std/substrate.dag The Rust witness advanced faster than the .dag constructor authority → either add the same tracked constructor-validation asymmetry comment/trigger used by ParamRef and TransformRef, or land the .dag-side constructor authority now.

⚠️ The main authority mismatch is fixed, but the new substrate witness needs tracked constructor-validation debt before it lands.

Comment thread src/v3/std/substrate.dag
type BindNodeId {
node: NodeId
}

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: BindNodeId is a substrate handle but the new .dag record is directly forgeable and lacks the Track 9 constructor-validation asymmetry/dissolution trigger that P2/P5 require for witness carriers.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: cursor / composer-2
  • Commit: ab3f4a81 · Trigger: schedule
  • Comparison: origin/main @ 94c479cf ... review/pr-1548-ab3f4a81 @ ab3f4a81
  • Thinking: 37s wall

Findings

None. The diff introduces BindNodeId as a substrate-backed witness (src/v3/std/substrate.dag, new BindNodeId + UserDefined(BindNodeId)), mirrors it in Rust (src/v3/compiler/src/dag.rs around the new struct and ArrowBody::UserDefined), and wires construction through BindNodeId::from_bind_node where arrow bodies are installed (src/v3/compiler/src/lower.rs, src/v3/compiler/src/infer.rs). That matches boundary discipline / single authority (fact lives in one typed place instead of every consumer re-checking NodeId → Bind), and API-level enforcement relative to the prior pattern of repeated .as_bind().expect(...).

Places that used to skip on a non-bind (continue / None) now call .bind(dag) (src/v3/compiler/src/infer.rs e.g. predicate_info, resolve_lambda_parameter_types, validate_user_defined_function_signatures). That is a deliberate tightening: once UserDefined carries BindNodeId, an inconsistent DAG is meant to be unreachable except bugs; emit keeps a typed error path where appropriate (src/v3/compiler/src/emit/rust_target.rs via bind_opt).

Bootstrap churn is large but mechanically tied to the substrate snapshot/regen path (bootstrap_generated*.rs, manifest hash line in parse_corpus_manifest.txt); nothing in that contradicts the rubric beyond normal generated-artifact noise.

Verdict

APPROVE — Scoped modeling fix: user-defined arrow bodies bind through a typed witness in substrate and Rust, consumers updated consistently, no concrete clash with INVARIANTS / modeling-discipline / CODING / TESTING for this diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the blocking Track 9 constructor-validation finding against 9fd466c2: valid. The substrate authority had BindNodeId, but it did not yet carry the tracked constructor-validation asymmetry / dissolution trigger used by sibling witness carriers like ParamRef and TransformRef.

Addressed on current head a1ca9b3b9:

  • Added the Track 9 constructor-validation asymmetry receipt beside BindNodeId in src/v3/std/substrate.dag.
  • The receipt names Rust BindNodeId::from_bind_node(dag, id) as today’s fail-closed constructor and the Lane 3c self-hosted substrate constructor authority as the dissolution trigger.
  • Regenerated bootstrap_generated.rs and bootstrap_generated_without_parse_surface.rs.
  • Refreshed parse_corpus_manifest.txt.

Validation run:

CARGO_TARGET_DIR=/tmp/gunbc-1548-bind-doc-target RUSTC_WRAPPER= cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify
CARGO_TARGET_DIR=/tmp/gunbc-1548-bind-doc-target RUSTC_WRAPPER= cargo test -p v3-compiler --test integration refresh_handwritten_parse_snapshot_manifest -- --ignored
cargo fmt --all --check
git diff --check

All passed.

— sent from jolly-ram-908

@briansrls
briansrls merged commit 0427f96 into main May 3, 2026
briansrls added a commit that referenced this pull request May 3, 2026
Per codex review on 0e0dfa8 (non-blocking improvement): the emitter row
flipped to Retired with the count delta but was not added to the "De Facto
Closed Or Cleanup-Only Rows" enumeration alongside the other PR #1548-class
retirements. Adds it as item 5 between Go UnknownVariant (PR #820) and the
E-M carrier-parity note; renumbers subsequent items 5→6, 6→7.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 3, 2026
…t) (#1564)

* docs(r3): retire emitter as_bind().expect() debt row (PR #1548 receipt)

PR #1548 (`0427f96f7`) landed the typed `BindNodeId` witness on
`ArrowBody::UserDefined`, retiring the six emitter panic paths surfaced as
Exploratory Finding 8. All cited sites now consume `(*bind_id).bind(self.dag)`;
the guarded `rust_target.rs:2503` site uses `.bind_opt(dag)` returning a
typed `EmitError::MalformedUserDefinedCallable`. The local-typed-error path
was rejected at design split as parallel-representation debt against the
substrate fix.

This PR closes the docs receipt:

- ROADMAP.md Exploratory Finding 8 — flipped to RETIRED with PR #1548
  receipt; preserved historical finding text and noted the chosen
  `BindNodeId` dissolution path.
- docs/debt/r3-debt-paydown-ledger-2026-05-02.md row 92 — flipped from
  Open to Retired; baseline counts updated (Open 60→59, Retired 3→4);
  highest-leverage list item 2 removed and remaining items renumbered;
  Substrate fail-closed mini-bundle scope adjusted.

R3 debt receipt: Debt paid (via Substrate #1548) for ledger row 92 /
ROADMAP.md Exploratory Finding 8.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): list emitter as_bind() retirement in De Facto Closed rows

Per codex review on 0e0dfa8 (non-blocking improvement): the emitter row
flipped to Retired with the count delta but was not added to the "De Facto
Closed Or Cleanup-Only Rows" enumeration alongside the other PR #1548-class
retirements. Adds it as item 5 between Go UnknownVariant (PR #820) and the
E-M carrier-parity note; renumbers subsequent items 5→6, 6→7.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): drop ambiguous "previously item N" labels in highest-leverage footnote

Per cursor review on 5070873 (APPROVE_WITH_COMMENTS): the footnote claimed
"Previously item 3 — Go UnknownVariant" which was correct against the
pre-both-retirements 10-item list but ambiguous against the post-merge
pre-renumber state where item 3 was Bootstrap diagnostics-empty gate.

Drop the numeric labels and reference both retired targets by content alone;
no information lost, no positional ambiguity.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant