binding_id soundness (#4587): declaration identity for PD-3 and upstream branding

[briansrls]

Summary

Implements the #4587 brand-identity path for v2 type declarations: BindingId, TypeDeclBinding, allocator state, Node.binding_id, and TypeEnv.decl_registry are the declaration identity channel. Declaration ids originate at build_type_env registration, are preserved through structural resolution with with_preserved_binding_id, and PD-3 compatibility compares declaration identity through binding_id instead of spelling/ident_span.

Phase-1 scope is intentionally single-module/user-module dogfood. Same-spelling cross-module behavior is guarded by an explicit witness; full phase-2 cross-module same-spelling claims remain out of scope.

Contract / Proof Notes

• Authority-only origination: alloc_binding_id is the sole DAG mint path; register_type_decl_binding stamps from declaration authority during type-env registration.
• Nominal boundary: generated Rust emits pub struct BindingId(i64) with private inner value and pub(crate) fn mint; Node, TypeDeclBinding, decl_registry, duplicate tracking, and comparison paths carry BindingId, not raw Int/i64.
• BindingId-first lookup: lookup_type_for consults decl_registry[binding_id].binding_key and returns that name-keyed binding only after verifying it carries the requested BindingId; otherwise it falls back to carrier_bindings[binding_id]. Stamped nodes do not resolve by authored spelling.
• Registry-before-consumer order: register_type_decl_binding mints, stamps, and inserts the matching decl_registry row in one accumulator update before pre_local_env is merged; imported hidden carriers are collected from already-built parent TypeEnvs whose registries are merged into import_env; build_type_env_unresolved does not stamp local binding_ids, so there is no stamped-local/empty-registry partial rollout.
• TypeEnv map discipline: bindings remains the visible/name-keyed namespace, decl_registry is the BindingId-to-declaration-authority table, and carrier_bindings is the hidden structural dependency carrier for non-visible imported dependencies. They coexist during phase 1 because visibility, declaration authority, and hidden transitive structure are distinct facts; stamped lookup checks decl_registry first and validates the resolved binding carries the requested BindingId, then uses carrier_bindings only for hidden dependencies, and never falls back to authored spelling for stamped nodes. merge_envs merges declaration authority through merge_decl_registry_state, which coalesces only identical TypeDeclAuthority and records duplicate BindingIds as diagnostics.
• No spelling-key stamp path: binding_key remains lookup metadata only; stamping is not fed by spelling/name/intern key.
• Declaration authority: TypeDeclBinding carries TypeDeclAuthority { module_name, decl_name, decl_span }; duplicate BindingId merge coalesces only when authority matches exactly, otherwise fails closed via duplicate diagnostics.
• Atomic identity swap: with_authored_identity / ident-span grafting is gone; structural rebuilds use with_preserved_binding_id / node_with_preserved_binding_id.
• Direct-call diagnostics: direct_call_arg_span_skips is removed; module_skips_direct_call_arg_check is hard false, with no path-prefix skip for src/v2, src/v3, src/v4, dsl/std, dsl/v4, or dsl/extdeps.
• Imported structural dependencies are carried hidden for branding/field-access without becoming visible names.
• Synthetic Refined heads carry no binding_id; kernel container shells compare structurally and recurse into branded elements.
• node_type_compatible leaf comparison fails closed when exactly one non-kernel side carries binding_id; same binding accepts only after cardinality gates pass.
• BindingId comparison lives in node_type_compatible / PD-3. exact_structural_equality_zip_fold / Value::eq were not edited, so the provenance A-pivot equality work is not entangled.

Current-Head Execution Receipts

Current head: d0d8819d539688ab7eddf7d0444d39431a4cd4f4.

• ctrl-build -- timeout 900s cargo run -p v2-compiler --bin regen_stage0 -> regen_stage0: wrote 68 generated stage0 files., zero hard diagnostics.
• ctrl-build -- timeout 600s cargo test -p v2-compiler-tests 'pd3_' -- --nocapture -> 18 passed, 0 failed. Includes the ported adversarial suite plus adv_same_named_decls_in_different_modules_must_stay_distinct.
• ctrl-build -- timeout 600s cargo test -p v2-compiler-tests infer_semantics -- --nocapture -> 44 passed, 0 failed.
• ctrl-build -- timeout 300s cargo test -p v2-compiler-tests anthropic_tool_result_content_rejects_legacy_string_slot -- --nocapture -> 1 passed, 0 failed.
• Pipeline suite delta: branch ctrl-build -- timeout 1200s cargo test -p v2-compiler-tests pipeline -> 336 passed, 24 failed, 41 ignored. Current main same command -> 335 passed, 24 failed, 41 ignored. Failure identity comparison: branch-only failures empty; main-only failures empty.
• v2 compiler lib delta: branch ctrl-build -- timeout 1200s cargo test -p v2-compiler --lib -> 17 passed, 5 failed, 5 ignored. Current main same command -> 17 passed, 5 failed, 5 ignored. Failure identity comparison: branch-only failures empty; main-only failures empty.
• Workspace delta: branch and current main ctrl-build -- timeout 1800s cargo test --workspace --all-targets both fail only workflow_no_path_regex_policy_ci_yml because the test invokes git ls-files from a non-repo parent (/home/briansrls/.worktrees on branch, /tmp on main). New workspace failures empty by identity.

Sole-Mint Proof

• rg -n "BindingId \\{ value:" src/v2 -g '*.dag' -> only src/v2/04_env.dag:58, inside alloc_binding_id.
• rg -n "BindingId::mint\\(" src/v2/stage0/src -g '*.rs' | rg -v 'v2_compiler_emit_rust.rs' -> only src/v2/stage0/src/v2_compiler_infer_env.rs:73, the generated allocator.
• rg -n "\\bBindingId\\(" src/v2/stage0/src -g '*.rs' | rg -v 'v2_compiler_emit_rust.rs' -> only pub struct BindingId(i64) and BindingId(value) inside the private mint implementation in v2_std_core.rs.
• No public From<i64>, raw constructor, as_binding_id, or raw diagnostic extractor. node_has_binding_id grep hits are read-only comparison helpers, not construction.

Earlier Focused Receipts Preserved

• ctrl-build -- timeout 900s cargo test -p v2-compiler-tests pipeline::chained_type_alias_field_access -- --exact --nocapture -> 1 passed.
• ctrl-build -- timeout 900s cargo test -p v2-compiler-tests pipeline::indirect_type_alias_cycles_do_not_recurse_forever -- --exact --nocapture -> 1 passed.
• ctrl-build -- timeout 900s cargo test -p v2-compiler-tests diagnostics -- --nocapture -> 12 passed, 0 failed, 1 ignored.

Readiness

Parent sign-off posted. Waiting on 2 dashboard approvals + CI green for operator merge. Do not merge from this worker session.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 0b2c48a0 · Trigger: schedule
• Thinking: 280s wall

---

BLOCKING (3)

Root Cause

• src/v2/00_core.dag Node updates are still hand-maintained record rebuilds → add a canonical identity-preserving Node reconstruction/update API or update every reconstruction in this PR with an explicit preserve/drop reason.
• src/v2/04_env.dag Name lookup and binding-id lookup are modeled as separate payload-owning registries → make one declaration table authoritative and have alternate indexes store only keys/references.
• src/v2/04_env.dag BindingId freshness is local while environment merge assumes global uniqueness → namespace IDs by module or merge registries with duplicate-ID diagnostics.

⚠️ The binding-id direction is useful, but the new substrate identity needs facts-flow, single-authority, and collision guarantees before landing.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 66609328 · Trigger: schedule
• Thinking: 368s wall

---

BLOCKING (2)

Root Cause

• src/v2/00_core.dag declaration identity is modeled as an unconstrained scalar instead of a nominal/freshness-checked carrier → make BindingId the boundary type everywhere and route construction through the allocator/diagnostic API.
• src/v2/04_infer.dag PD-3 compatibility exceptions are encoded as source-path heuristics instead of a typed, bounded deferral → remove the span skip or constrain it behind a documented trigger that still preserves fail-closed diagnostics.

⚠️ The binding-id direction is good, but the raw identity carrier and broad diagnostic bypass need fixes before landing.

[briansrls]

Verified the current-head codex blockers against #4615 at 6660932. They are valid and I routed fixes to the worker. The diff still models declaration identity as raw Int (, , allocator returns Int), so BindingId is not yet the nominal/freshness-checked boundary type required by #4587. The diff also adds , a broad source-path heuristic bypass for PD-3 diagnostics; that must be removed or replaced with a typed, bounded deferral that preserves fail-closed diagnostics. #4615 remains draft until these are fixed, the PR body carries receipts, and parent signs off. — sent from bright-owl-653

[briansrls]

Correcting shell-quoting damage in my prior comment. Verified the current-head codex blockers against #4615 at 6660932; they are valid and routed to the worker. The diff still models declaration identity as raw Int: type BindingId = Int; Node.binding_id: Int?; TypeDeclBinding.binding_id: Int; allocator returns Int. BindingId needs to be the nominal/freshness-checked boundary type required by #4587. The diff also adds direct_call_arg_span_skips, a broad source-path heuristic bypass for PD-3 diagnostics; that must be removed or replaced with a typed, bounded deferral that preserves fail-closed diagnostics. #4615 remains draft until these are fixed, the PR body carries receipts, and parent signs off. — sent from bright-owl-653

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e6ba8930 · Trigger: schedule
• Thinking: 392s wall

---

BLOCKING (1)

Root Cause

• src/v2/04_env.dag TypeDeclBinding has no module-level declaration authority, only local intern key/name → add a canonical declaration key/span/module and only coalesce duplicate BindingId entries when that authority matches.

⚠️ The BindingId merge guard still has a false-negative collision path that should be closed before landing.

[briansrls]

Verified the e6ba893 codex blocker against current #4615 head d2969e5. It is still valid: TypeDeclBinding still carries only binding_id, binding_key, name, and provenance, and merge_decl_registry_state coalesces duplicate BindingId entries when binding_key/name match. binding_key is still a spelling/intern key, not module-level declaration authority, so same-spelling declarations from different modules can be false-coalesced. This needs a canonical declaration authority key (module identity plus declaration span/source location, or equivalent closed declaration identity), and duplicate BindingIds should coalesce only when that authority matches exactly; otherwise fail closed with diagnostics. #4615 remains draft. — sent from bright-owl-653

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c1ab9014 · Trigger: schedule
• Thinking: 418s wall

---

BLOCKING (1)

Root Cause

• src/v2/00_core.dag Node.binding_id uses None for both genuinely unbranded kernel nodes and missing/dropped declaration identity → split that state or make one-sided BindingId comparisons fail closed after lookup.

⚠️ One remaining identity-erasure path can still false-accept branded types.