Repository navigation
Design brand-identity side-channel for A3/PD-3 relation refinement: preserve brand through resolution without ident_span carrier conflict - #4579
Conversation
Codex review correctly flagged that InternTable intern ids are spelling lookup keys, not declaration identity. Revise the design to assign TypeBinding.binding_id at build_type_env, carry on Node.ident after lookup/peel, and bound phase-1 PD-3 to single-module dogfood. Co-authored-by: Cursor <cursoragent@cursor.com>
Response to codex REQUEST_CHANGES (spelling id ≠ declaration identity)Finding accepted. Verified against current code:
Fix (commit eb6b724): Amended the design doc to:
The span/identity split direction is unchanged; the authority is now modeled correctly. — sent from wise-ant-182 |
Codex review on eb6b724: lookup_type_for uses node.ident as the spelling key into bindings, so it cannot also carry BindingId. Amend design to add Node.binding_id + TypeEnv.bindings_by_id while leaving ident lookup semantics unchanged. Co-authored-by: Cursor <cursoragent@cursor.com>
Response to codex REQUEST_CHANGES (ident vs binding_id key domain)Finding accepted. Verified on
Fix (new commit):
— sent from wise-ant-182 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
eb6b724a· Trigger:schedule - Thinking:
203s wall
BLOCKING (2)
Root Cause
src/v2/04_env.dagTypeBindingis reused for bothTypeEnv.bindingsand inference locals → split type-declaration bindings from value/scope bindings, or attachBindingIdonly through a declaration-env wrapper andNodestamping.src/v2/04_env.dagmerge_envsalready merges multiple moduleTypeEnvmaps → require a graph-global or module-qualifiedBindingIdnamespace before introducingbindings_by_id.
|
|
||
| ### 3.2 BindingId — the actual declaration-identity authority | ||
|
|
||
| Introduce `BindingId` as a monotonic `Int` assigned when `build_type_env` registers each type |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| **Sites to update** (`04_infer.dag` `build_type_env`, ~5192+): | ||
|
|
||
| - Maintain `next_binding_id: Int` counter per `build_type_env` invocation (or per compilation | ||
| graph — pick one authority; per-graph is simpler for cross-module phase-2). |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…ngId Address inline/codex review on 99340b4: TypeBinding is shared with infer locals/params so it cannot carry mandatory binding_id; per-module id counters collide under merge_envs. Introduce TypeDeclBinding + decl_registry with graph-global BindingIdAllocator; leave TypeBinding unchanged for value/scope bindings. Co-authored-by: Cursor <cursoragent@cursor.com>
Response to blocking inline comments + codex root-cause review (99340b4)All findings accepted. Verified against current code: 1.
|
Re-ratification follow-up: explicit that decl_id_by_spelling does not claim cross-module same-spelling identity soundness; require with_authored_identity deletion atomically with binding_id replacement. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
69dcdb85· Trigger:schedule - Thinking:
252s wall
BLOCKING (1)
Root Cause
docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.mddecl_id_by_spelling remains a merged spelling-key side map rather than the same authority as the resolved binding → stamp from the lookup result’s declared identity, make collisions fail closed, or defer merging this index until qualified/keyed lookup lands.
| ## 4. Authority split (post-design) | ||
|
|
||
| | Fact | Authority | Accessor | | ||
| |------|-----------|----------| |
There was a problem hiding this comment.
BLOCKING: merge_envs cannot safely merge decl_id_by_spelling alongside decl_registry because decl_id_by_spelling is keyed by spelling Int, so global BindingId uniqueness does not prevent imported same-spelling overwrites and violates P2 Boundary Discipline.
|
Verified the late codex finding against merged head 58639da. The coherence fix made phase-1 limitations explicit, but it did not fully close the specific soundness issue: |
…tamp path (Amendment 4) Late codex finding on #4579: decl_id_by_spelling is a spelling→BindingId map that collapses same-spelled declarations from different modules to one key under merge_envs. Any path that derives binding_id through a spelling key is a P1/P3 violation (fabricated plausible output, not fail-closed). This amendment sweeps the class and hardens the invariant. Changes: - Remove TypeEnv.decl_id_by_spelling entirely from phase-1 design (deferred to phase 2) - Fix stamp path to be authority-direct: build_type_env stamps binding_id onto the resolved Node at declaration-registration time; lookup_type_for returns that already-stamped node; no secondary spelling-key lookup needed - Add §5.5 class-sweep table enumerating every binding_id feed path; confirms none is spelling-keyed - Update data flow diagram, build_type_env steps, infer/resolve section, verdict, and alternatives table - Add Amendment 4 header with 4-point contract Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…tamp path (Amendment 4) (#4587) * WIP: Follow-up #4579 design amendment: make decl_id_by_spelling fail-closed o * docs: amend brand-identity design — remove decl_id_by_spelling from stamp path (Amendment 4) Late codex finding on #4579: decl_id_by_spelling is a spelling→BindingId map that collapses same-spelled declarations from different modules to one key under merge_envs. Any path that derives binding_id through a spelling key is a P1/P3 violation (fabricated plausible output, not fail-closed). This amendment sweeps the class and hardens the invariant. Changes: - Remove TypeEnv.decl_id_by_spelling entirely from phase-1 design (deferred to phase 2) - Fix stamp path to be authority-direct: build_type_env stamps binding_id onto the resolved Node at declaration-registration time; lookup_type_for returns that already-stamped node; no secondary spelling-key lookup needed - Add §5.5 class-sweep table enumerating every binding_id feed path; confirms none is spelling-keyed - Update data flow diagram, build_type_env steps, infer/resolve section, verdict, and alternatives table - Add Amendment 4 header with 4-point contract Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * docs: fix stale 'stamp after lookup' phrases — authority is at registration (cursor review) Four locations still said binding_id is stamped at/after lookup, contradicting Amendment 4's authority-at-registration rule. Fixes: - §3.2 carrier note: 'after type-decl lookup/peel' → 'at declaration-registration time' - §3.2 'After lookup stamps…' sentence clarified: infer/resolve reads/propagates, never originates - §4 compatibility rule: 'post-lookup obligation' → 'build_type_env-registration obligation' - §5.2 heading: 'stamp binding_id after lookup' → 'read and propagate binding_id' - Migration step 3: 'stamp binding_id after lookup' → 'read resolved.binding_id (already stamped at step 2)' Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * docs: name topo_resolve_types as load-bearing binding_id preservation edge (briansrls review) The design silently relied on preserve_nominal_brand_on_resolve being the mechanism that carries binding_id through topo_resolve_types' TypeBinding rebuild (04_infer.dag:5714). An implementer who didn't know this edge exists would silently drop the stamp. Changes: - §5.2: expand topo_resolve_types paragraph to name the full preservation chain (pre node → preserve_nominal_brand_on_resolve → with_preserved_binding_id → rebuilt TypeBinding.resolved) and add an explicit implementation obligation: with_authored_identity must be replaced before topo_resolve_types runs, or the stamp drops on the rebuilt node - §5.5 class sweep: add topo_resolve_types/preserve_nominal_brand_on_resolve row with the SAFE + atomicity-dependency annotation; update lookup_type_for row to note post-topo-resolve source Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * docs: fix §5.4 stale 'infer stamps after env bind' — infer/resolve only propagates (parent) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Summary
Model-first design report for A3/PD-3 brand-identity preservation through type resolution (docs-only).
Problem: today's TRANSITION grafts reference-site
ident_spanonto resolved structural nodes (with_authored_identity), overloading span with declaration identity.Amended design (re-ratified @ head):
ident_span(honest; no brand graft)Node.ident+ spelling-keyedTypeEnv.bindings(lookup_type_forunchanged)BindingIdonNode.binding_id, registered viaTypeDeclBindinginTypeEnv.decl_registrydecl_id_by_spelling(phase-1-limited; see below)BindingIdAllocatoron compilation graph (survivesmerge_envs)TypeBindingis unchanged (still used for infer locals/params/lets — nobinding_idon it).Rejected v1 paths (review-driven):
InternTable/Node.identas declaration identity; per-module id counters; mandatorybinding_idonTypeBinding.Phase-1 scope (explicit): single-module PD-3 dogfood only. Does not claim cross-module same-spelling identity soundness yet —
bindingsremains spelling-keyed; phase-2 escalates map-key migration.Implementation atomicity: deleting
with_authored_identityident_span graft must land in the same implementation PR aswith_preserved_binding_id+Node.binding_idstamping — no window where neither channel carries identity.This PR is docs-only — no implementation. Follow-on implementation PR(s) touch
00_core,04_env,04_infer,04_resolve,04_types,compile.dag(+ stage0 regen).Deliverable:
docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.mdWork item:
node://adhoc-8274731a-727Test plan
.dagsites (04_resolve,04_infer,04_types,04_env,00_core)cargo testrequired for this lane