docs: amend brand-identity design — remove decl_id_by_spelling from stamp path (Amendment 4)

[briansrls]

Summary

Design amendment to docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.md (follow-up to #4579). Late codex finding: decl_id_by_spelling as designed in #4579 is a spelling→BindingId map that routes the binding_id stamp through a spelling key — a P1/P3 violation.

This PR is docs-only. No implementation files changed.

Work item: node://adhoc-9d1bcff7-697

---

4-point contract (acceptance criteria)

1. Authority-only binding_id stamping. Node.binding_id is set only from a value produced by alloc_binding_id (direct) or copied from a node already stamped by alloc_binding_id (transitive graft). build_type_env stamps binding_id onto the resolved Node at declaration-registration time — not after lookup, not from a spelling key. The stamp is carried on the Node value shared between TypeDeclBinding.resolved and TypeBinding.resolved, so any subsequent lookup_type_for returns a node that already carries the stamp.

2. decl_id_by_spelling removed from the soundness-critical stamp path. The field does not exist in phase-1 TypeEnv. The stamp path in §5.2 is now authority-direct: after lookup_type_for returns TypeBinding.resolved, the caller reads resolved.binding_id — no secondary Map<Int, BindingId> lookup.

3. Any future spelling→id index must be lookup-only, fail-closed on collision, and is deferred to phase 2. If a spelling→BindingId index is eventually needed for cross-module lookup optimisation it must: (a) be constructed fail-closed (collision = ambiguous/absent, never silent winner-pick), (b) never be a stamp source, and (c) only be introduced with cross-module collision tests. Phase 1 ships without it.

4. Class sweep: no spelling-keyed path feeds binding_id. §5.5 enumerates every path that writes Node.binding_id. All are authority-direct (from alloc_binding_id directly or transitive graft of an already-stamped node). The one spelling-keyed path (decl_id_by_spelling lookup → stamp) is explicitly listed as REMOVED.

---

Changed claims

Location	Old	New
TypeEnv struct (§3.2)	decl_id_by_spelling: Map<Int, BindingId> present	Field absent — comment explains deferral
build_type_env steps (§5.1)	Step 3 records decl_id_by_spelling[item_ident] = binding_id; step 4 stamps node	Steps renumbered: stamp at registration (step 2), no decl_id_by_spelling entry
Stamp path (§5.2)	"resolve declaration identity via decl_id_by_spelling → decl_registry"	"read binding_id directly from the resolved Node returned by lookup_type_for"
Data flow diagram (§5)	decl_id_by_spelling → TypeDeclBinding node in infer/resolve subgraph	Removed; stamp node moved into env_bind subgraph at registration
Phase-1 scope (§3.3)	"decl_id_by_spelling is honest but phase-1-limited"	"decl_id_by_spelling is deferred entirely (Amendment 4)"
Alternatives table (§3.4)	No entry for decl_id_by_spelling as stamp path	Two new rows: Reject (stamp source) + Defer (lookup-only)
Verdict / non-implementation (§9)	Lists TypeEnv.decl_id_by_spelling as new type	Removed from new-types list; explicit "do not introduce" constraint added
§5.5 (new)	Absent	Class-sweep table: 7 rows covering every binding_id feed path

Test plan

• Docs-only change — no cargo test required
• Amendment 4 header with 4-point contract added at top of design doc
• §5.5 class-sweep table enumerates every binding_id feed path; confirms none is spelling-keyed
• All stale decl_id_by_spelling references in the design doc updated

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2a038c4c · Trigger: schedule
• Thinking: 288s wall

---

BLOCKING (1)

Root Cause

• src/v2/04_infer.dag resolve_env_bindings/topo_resolve_types rewrites TypeEnv.bindings after local registration → add an explicit obligation to preserve binding_id through those resolver rebuilds, or stamp the final resolved binding from TypeDeclBinding before lookup consumers run.

⚠️ One load-bearing stamp-path edge is missing from the amended design.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b29b29ba · Trigger: schedule
• Thinking: 207s wall

---

✅ Amendment 4 removes spelling-key identity from the stamp path and I found no remaining blocking contradictions with the thesis or invariants.

[briansrls]

This finding was addressed in commit cdd8817 (pushed before b29b29b). The current HEAD already names the topo_resolve_types preservation edge explicitly:

• §5.2 has a dedicated topo_resolve_types preservation edge (load-bearing — must not be missed) paragraph (line 349) naming the full chain: pre = binding.resolved → preserve_nominal_brand_on_resolve → with_preserved_binding_id → rebuilt TypeBinding.resolved retains stamp.
• §5.5 sweep table has the topo_resolve_types / preserve_nominal_brand_on_resolve rebuild row confirming it's SAFE with the atomicity dependency noted.
• lookup_type_for row updated to say "set at build_type_env registration and preserved through topo_resolve_types via with_preserved_binding_id".

The inline comment appears to have been written against an earlier SHA and relayed after the fix landed. No code change needed.

— sent from swift-moth-293

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2bb50875 · Trigger: schedule
• Thinking: 186s wall

---

Non-blocking — Strengths

• docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.md The amendment removes spelling-key identity from the stamp path and keeps declaration identity single-authority and fail-closed.

✅ No blocking concerns found.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 179310d0 · Trigger: schedule
• Thinking: 252s wall

---

✅ The docs-only amendment removes spelling-key identity from the stamp path and keeps BindingId authority registration-direct with no blocking concerns.