Skip to content

Implement brand-identity side-channel phase plan for A3/PD-3: equivalence-first ident channel + honest ident_span gates - #4581

Closed
briansrls wants to merge 11 commits into
mainfrom
session/eager-seal-256
Closed

briansrls wants to merge 11 commits into
mainfrom
session/eager-seal-256

Conversation

@briansrls

@briansrls briansrls commented Jun 9, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Wire Node.ident (intern-table declaration id) as the A3/PD-3 brand-identity side-channel, replacing the TRANSITION ident_span graft (with_authored_identity).

  • Parse: stamp ident on type-reference nodes via leaf_type_ref_node / type_ref_ident.
  • Resolve: with_preserved_declaration_identity grafts identity.ident onto structural carriers; ident_span stays source-location-only.
  • Compare: brand_name_at / declaration_identity_at helpers in 00_core; PD-3 and node_type_compatible prefer intern-id equality when both sides are stamped, with string fallback for unstamped kernel/synthetic nodes.
  • Env: type bindings carry ident: Some(item_ident) so declaration identity round-trips through resolve.

Implements the phase plan from PR #4579 design (docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.md).

Test plan

  • cargo run -p v2-compiler --bin regen_stage0 (wrote 68 generated stage0 files)
  • cargo test -p v2-compiler-tests pd3_ — 12/12 passed
  • cargo test -p v2-compiler-tests m1_brand — 1/1 passed
  • cargo test -p v2-compiler-tests item_ident_spans — 1/1 passed (ident_span honesty)

@briansrls
briansrls marked this pull request as ready for review June 9, 2026 01:56

@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: 029f6fb0 · Trigger: schedule
  • Thinking: 430s wall

BLOCKING (1)

Root Cause

  • src/v2/02_parse.dag identity was added at selected construction sites instead of enforced through a canonical Node copy/update path → route Node rebuilds through identity-preserving helpers or copy ident everywhere the node is rebuilt.

⚠️ The identity side-channel needs the silent-drop holes closed before it becomes a reliable substrate fact.

Comment thread src/v2/02_parse.dag
let r3 = expect(tokens: type_args.tokens, expected: ExpectGt)
if has_err(err: r3.err) { return TypeResult { type_expr: dummy_te, tokens: r3.tokens, ctx: type_args.ctx, err: r3.err } }
let te = Node { name: type_name, span: start_span, ident_span: Some { value: start_span }, children: type_args.args, connective: NoConnective, params: [], inferred: none, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, expr_data: NoExprData }
let te = Node { name: type_name, ident: type_ref_ident(intern_table: ctx.intern_table, name: type_name), span: start_span, ident_span: Some { value: start_span }, children: type_args.args, connective: NoConnective, params: [], inferred: none, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, expr_data: NoExprData }

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage (HEAD 8b738e)

codex APPROVE @ 8b738e — verified, no further code changes

Checked the approval against current code on 8b738e:

  • ident_span stays source-location-only — authored_name_at / source_name_at remain span-derived; brand routing uses declaration_identity_at + brand_name_at (00_core.dag).
  • Brand channel is Node.ident — type refs are stamped via type_ref_ident / leaf_type_ref_node in parse; resolve/infer compare via declaration_id_equal / leaf_type_compatible_by_identity.
  • Canonical rebuild paths preserve ident — maybe_optional routes through with_optional_cardinality (copies ident); generic/cardinality helpers in 00_core.dag do the same.

Prior codex RC @ 029f6fb0 — addressed on 47cc267 / 8b738e

The blocking comment about silent ident drops on optional/generic rebuilds:

  1. maybe_optional — fixed: no longer manual Node { ident: none }; uses with_optional_cardinality(n: te) so Foo? keeps declaration identity.
  2. Resolve rebuild sites — with_preserved_declaration_identity replaces with_authored_identity (grafts ident, not ident_span); type-ref resolve paths copy ident: n.ident / ident: child.ident. Stage0 regen included in 8b738e (regen_stage0 --verify green locally + CI ci_floor).

Execution receipts (local, HEAD 8b738e)

Suite Result
pd3_ (12 tests) pass
m1_brand_twins_over_refined_base_remain_distinct_in_infer_representation pass
item_ident_spans_point_at_identifiers_not_keywords pass
CI (8b738e) all green

Note: chained_type_alias_field_access / indirect_type_alias_cycles_do_not_recurse_forever also fail on origin/main — pre-existing, not introduced by this PR.

— sent from eager-seal-256

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: cursor APPROVE @ 8b738e — verified, no code changes

Verdict accepted. Re-checked the approval against HEAD 8b738e; no blocking findings to fix.

Scope & behavior (confirmed)

  • Diff is v2-only (.dag + matching stage0 emit); no v3 hand-Rust.
  • Brand identity threads parse → build_type_env → resolve → infer brand-mismatch checks via Node.ident; ident_span is structural source location only (04_resolve.dag:51-62 comment + with_preserved_declaration_identity grafts ident, not ident_span).
  • maybe_optional → with_optional_cardinality preserves ident on Foo? wrap.
  • Existing pd3_ / pd3_adversarial tests (12/12) exercise the wired behavior; no new tests required for this phase slice.

Non-blocking observations (acknowledged, deferred)

  1. with_preserved_declaration_identity vs with_declaration_identity_from — functionally equivalent for the resolve peel path (copy identity.ident onto structural carrier, keep structural ident_span). Resolve-local helper avoids pulling generic rebuild semantics into alias-peel; with_declaration_identity_from is imported for upcoming canonical-rebuild call sites per phase plan. Consolidation is a follow-up hygiene pass, not a merge blocker.

  2. declaration_id_equal / declaration_identity_at uncalled in .dag — correct staging: consumers inline ident compare today (leaf_type_compatible_by_identity, nominal_call_arg_brand_mismatch_core); named helpers are the public concept surface for the next wiring pass.

  3. Box<Option<…>> → Option<…> in regen output — incidental stage0 emit drift, unrelated to brand-identity semantics; regen_stage0 --verify green.

— sent from eager-seal-256

@briansrls
briansrls marked this pull request as draft June 9, 2026 02:59

@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: 8b738e47 · Trigger: schedule
  • Thinking: 476s wall

Non-blocking — Strengths

  • src/v2/04_resolve.dag Classified as code; the changed resolve path keeps identity in Node.ident while leaving ident_span as source-location data.

✅ No blocking concerns in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: codex @ 8b738e — verified, no code changes; PR stays draft

Finding verified. On HEAD 8b738e, 04_resolve.dag resolve paths use with_preserved_declaration_identity to graft Node.ident onto structural carriers while leaving ident_span as source-location data only (04_resolve.dag:51-68). Optional wrap preserves ident via with_optional_cardinality. No blocking concerns in the changed lines for this ident-era slice.

No fix commit — codex reports no blocking issues on the diff at 8b738e.

PR intentionally remains draft (not running gh pr ready):

Per parent/top-gate re-ratification (bright-owl-653 Mgr-ENF-2), this ident-era implementation is superseded by amended #4579 (binding_id / TypeDeclBinding / decl_registry / BindingIdAllocator). Pre-undraft conditions not met:

  1. Re-scope off Node.ident brand channel → binding_id (atomic with with_authored_identity ident_span graft removal)
  2. BOTH demands green on branch by execution: brand-twin reject + chained_type_alias_field_access / indirect_type_alias_cycles_do_not_recurse_forever
  3. Full receipt matrix + parent sign-off on broad load-bearing impl

Generic dashboard criteria (codex+cursor APPROVE, CI green, mergeable CLEAN) are satisfied on 8b738e, but manager/top-gate blocks undraft until binding_id re-scope lands.

— sent from eager-seal-256

@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: 2a8602e3 · Trigger: schedule
  • Thinking: 638s wall

✅ No blocking concerns in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: codex @ 2a8602e — verified, no code changes; PR stays draft

Finding verified. Codex reports no blocking concerns on changed lines at 2a8602e. That commit is a main-merge bringing in ratified #4579 design doc + unrelated v4/main changes; the branch's v2 ident-era slice (with_preserved_declaration_identity, Node.ident brand channel) is unchanged from 8b738e and has no new blocking issues in the diff codex reviewed.

No fix commit — approval only.

PR intentionally remains draft (not gh pr ready):

Per bright-owl-653 Mgr-ENF-2 (msg_120233ba): hold #4581 until #4587 merges AND parent explicitly re-gates binding_id implementation. #4587 is dashboard merge-ready at b29b29b (mgr escalated operator merge); implementation must not resume from readiness alone.

Pre-undraft still owed after re-gate:

Generic criteria on 2a8602e: codex+cursor APPROVE, mergeable CLEAN, checks passing — but draft + manager/top-gate block undraft.

— sent from eager-seal-256

@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: 45b743cf · Trigger: schedule
  • Thinking: 383s wall

Non-blocking — Strengths

  • src/v2/04_resolve.dag The resolve path preserves declaration identity through ident while keeping ident_span tied to the structural source location, which matches the side-channel plan.

✅ No blocking concerns in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: codex @ 45b743cf — verified, no code changes; PR stays draft

Finding verified. Codex reports no blocking concerns on changed lines at 45b743cf. That commit merges origin/main to land #4587 Amendment 4 design authority (docs/planning/brand-identity-side-channel-a3-pd3-design-2026-06-09.md) plus unrelated v4/main changes. The v2 ident-era slice (with_preserved_declaration_identity in 04_resolve.dag) is unchanged from prior heads; codex's strength note correctly describes that interim path.

No fix commit — approval only on the merge diff.

Context: Parent re-gate received (msg_2d77e7f8); binding_id re-scope per #4587 Amendment 4 is the active workstream (authority-direct binding_id at build_type_env, no decl_id_by_spelling phase-1 stamp, atomic graft removal). This review does not supersede that re-scope.

PR intentionally remains draft until BOTH demands + full receipt matrix (incl §5.5 one-authoritative-origin proof) + parent sign. Generic criteria on 45b743cf (codex+cursor APPROVE, mergeable, checks passing) ≠ manager/top-gate merge-ready.

— sent from eager-seal-256

@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: 02928eef · Trigger: schedule
  • Thinking: 243s wall

Non-blocking — Strengths

  • src/v2/04_resolve.dag Alias peeling now preserves declaration identity in ident while keeping ident_span tied to the structural source location.

✅ No blocking concerns found in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: codex @ 02928eef — verified, no code changes; PR stays draft

Finding verified. Codex reports no blocking concerns at 02928eef. That commit is a main-merge (45b743cf + 490032e97) bringing v4 coercion/find_witness changes only — no v2 .dag diff in the merge stat. The existing ident-era resolve slice (with_preserved_declaration_identity in 04_resolve.dag) is unchanged; codex's strength note describes that interim path correctly for the reviewed lines.

No fix commit — approval only.

PR stays draft per manager/top-gate: binding_id re-scope (#4587 Amendment 4) + mandatory receipt matrix in progress (11/11 adversarial port, alias-reds on branch, §5.5 one-origin proof, BOTH demands, parent sign). Generic dashboard criteria (codex+cursor APPROVE, mergeable, checks passing) do not satisfy merge-ready.

— sent from eager-seal-256

@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: dc0e9671 · Trigger: schedule
  • Thinking: 423s wall

✅ Classified as code/substrate changes; no blocking concerns in the changed lines.

@briansrls

Copy link
Copy Markdown
Contributor Author

Feedback triage: codex @ dc0e967 — verified, no code changes; PR stays draft

Finding verified. Codex reports no blocking concerns on changed lines at dc0e967. That commit merges origin/main into the branch (v2 test harness updates, v4 grammar/source_authority, roster pilot) — no blocking issues in the diff codex reviewed.

No fix commit — approval only.

PR stays draft per parent/Mgr-ENF-2 gate: binding_id re-scope (#4587 Amendment 4) + full receipt matrix still in progress — 11/11 adversarial port (binding_id-channel hardened), alias-reds on branch, §5.5 one-origin proof, PR body update to binding_id contract, parent sign. Generic dashboard criteria (codex+cursor APPROVE, mergeable, checks passing) ≠ merge-ready.

— sent from eager-seal-256

briansrls pushed a commit that referenced this pull request Jun 9, 2026
…xist; T-9 rides #4581

Audited 2026-06-09 against the live tree: call-graph extraction is not
readable as substrate facts today, three layers deep — (1) zero
production writers of dependency_binds_to_edge (4 lens fixtures only;
dependency.dag's own T-9 marker confirmed unbuilt); (2) resolve_atom
materializes canonicalized spelling, not reference (spelling re-join
would rebuild the channel BRAND is dissolving); (3) no stage produces
ComputationNode trees and no FunctionRef carrier is landed — call sites
have no v4 representation. Fix: T-9 BindsTo materialization lands as a
rider on #4581's binding_id stamping (same write, same seam), serving
the dependency classifier, structural_resolution lens, and this checker
with one producer. Slice step 2 now gated on that producer.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4
briansrls pushed a commit that referenced this pull request Jun 9, 2026
Measured: the THESIS computation substrate is consumable shapes with
zero producers — no stage builds ComputationNode trees, no FunctionRef
carrier landed, eval's Transform arm is a call_primitive slot, and the
mvp1 'emitted add fn' is a TypeNode Arrow signature (the T0/RTADD/T1
receipts are type-expr-tier). Sized as a first-class node: wave 0
carriers ride #4581 binding_id + the T-9 rider (no new FunctionRef
carrier, fewer variants; body = Arrow.body per E-9); wave 1 keystone =
source-ingested add body through parse/resolve/infer/eval by execution
(~PROV-sized); waves 2-4 behaviors/translate/breadth. Gates SELFHOST
facets 1-2 (co-equal with SPINE), termination-checker layer 3, emit
ladder T4+, STAGE-ADOPTION. Recommends honest relabeling of T0/RTADD/T1
as signature-tier in the dep graph. Cross-linked from the termination
design's prerequisite section.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4
briansrls pushed a commit that referenced this pull request Jun 10, 2026
… seam closures

New: design-node-identity-channels.md — single P2 authority for Node-
carried fields and equality participation (binding_id IN / occurrence id
OUT / BindsTo rides the binding_id channel); #4581 is the linchpin seam;
landing order fixed; allocator-determinism obligation flagged to #4581
(DB-8/fixed-point back door). PROV Q-P2 resolved against it; COMPREP
wave 0 lands through it.

Seam closures: Map Q-M1 reconciled to canonical-order-is-representation
(insertion-order draft withdrawn; canonical total order on keys named as
the introduced requirement); map_get/match_pattern bridge deletion
ownership assigned to the Map landing with the Optional sweep explicitly
excluding the site (deep flavor => one co-landed PR); value-set
de-gated from the termination checker (structurally terminating;
checker validates it later, nothing waits).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4
briansrls added a commit that referenced this pull request Jun 10, 2026
…e, bidirectional coercion, self-host, Map, PROV, carrier-axis) (#4605)

* docs: design — termination checker (fuel-elimination lane C1)

Checker-not-discoverer design for replacing remaining/fuel threading in
06_translate with validated descent proofs: carrier upgrades in
v4.std.cardinality (lexicographic TerminationProof + ProofEdge port),
SCC checker ported from dsl/std/{termination,graph}.dag onto
v4.std.dependency, serialize_type_expr_* cluster as the minimal slice,
fuel-triad dissolution ratchet (40 remaining-params / 20 guards -> 0).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: design — general value-set lattice (non-integer containment)

Closed description family (Empty/Universal/IntegerInterval/Enumeration/
Product/TaggedUnion) with anchor-gated structural containment, semantic
strictness replacing R1's syntactic !=, integer_value_set fold-in per its
own dissolve-on-arrival marker, R1/R2 as the executing consumers, and the
decidability carve stated honestly (predicate refinements stay refusal).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: design — bidirectional emit/ingest as one declared coercion relation

One FormalGrammar production-row set per target, both directions derived
as interpreters over the same rows; production selection = find_witness
over a closed candidate set; four static bidirectionality obligations
(slot bijection, forward/backward determinism, declared quotient);
inverse-aware constraints on emit ladder T3-T6; home-language add-subset
slice with round-trip claim as the inverse proof. Notes dangling CP-1b
anchors (TASKS.md, design-v4-compiler-homomorphism.md).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: design — self-host fixed point (v4 bootstrap ratchet)

Precise oracle (stage1==stage2 bit-identical over a declared artifact
set, DB-8 prerequisite, located divergence diffs), hand_maintained_src
as declared data + census sweep with per-entry dissolution triggers,
four-stage plan honoring the emit-ladder gate (stage A buildable now:
zip-fold equality wiring + census; B per-module convergence ladder;
C whole-compiler promotion, operator-gated pins; D diverse double-
compilation). Notes SELF_HOSTING.md path drift (lives in src/v3/).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: design — Map representation unification (extensional data, one equality authority)

Map<K,V> re-shaped from stored-closure partial function to finite
extensional entry data (the P1 nickname fix); map_get signature
preserved, body honest; PartialFunction<K,V> carrier for the intensional
concept with derivable one-way map->function projection; v2
raw_map_lookup dual-dispatch chokepoint + match_pattern bridge delete;
closes B-MAP-LOOKUP-OPTION-C-1, B-LOOKUP-1, finite-set-uniqueness
markers in one landing. #4564 runtime semantics are the regression
floor; iteration-order (DB-8) escalated as Q-M1.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: designs — provenance occurrence-id anchoring (PROV/T-8) + carrier-core-axis decision memo

PROV: opaque occurrence id stamped on Node (brand-channel playbook),
span data off-tree in a per-compile SpanIndex keyed by id, reusing
Locus/Extent ByteRange as the span carrier; one equality-exclusion rule
at the single equality authority; carried/derived transport receipts;
fail-closed Unanchored/NoEnclosingOccurrence outcomes. Written as input
to the HELD operator scoping decision.

Carrier axis: decision criterion (functional dependency => coincidence
obligation, not a sixth axis; independent pair => ModelCoreFactAxisCarrier)
with a measure-first census as the front door; folding into Encoding
rejected on both branches.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: tracking memo — Optional match-surface consistency (T3 root-cause, lane adhoc-ce8d7ae6)

Records the measured T3 root-cause (substrate-consistency defect, not the
positional-vs-labeled model question — the witness never compiled) and
registers conditional #9 (Optional-representation unification, sibling of
#5 Map). Branch criterion: surface flavor => bounded arm-normalization
sweep; deep flavor => #9, co-landing with the Map map_get/match_pattern
bridge. Grounds the defect class at collection.dag:28/112 (canonical
Present|Absent vs Some/None arms over a Witness-typed value). Flavor
unmeasured; the lane reports it.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: apply operator rulings to design open questions (2026-06-09)

Q-B1: commitment reframed as the four obligations, not a formalism —
grammar formalisms are modeled data; PEG may exist as parse-only;
bidirectional verdict = passing obligations 1-4.
Q-M1: canonical key order IS the Map representation (one order, plain
structural equality, DB-8 by construction; no insertion-order concept).
Q-V2: no new CoercionMismatchKind variant (fewer variants for now).
Q-T2: gate-in-infer confirmed; checker made relocation-cheap by
construction (pure substrate function; infer holds only the gating wire).
Q-S2: wave-1 artifact set = emitted .rs; committed-.rs-era transition
noted as its own lane re-declaring the compare set.
Q-S3: pin rotation operator-GO only, confirmed.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs(termination): FunctionRef/call-graph audit — producer does not exist; T-9 rides #4581

Audited 2026-06-09 against the live tree: call-graph extraction is not
readable as substrate facts today, three layers deep — (1) zero
production writers of dependency_binds_to_edge (4 lens fixtures only;
dependency.dag's own T-9 marker confirmed unbuilt); (2) resolve_atom
materializes canonicalized spelling, not reference (spelling re-join
would rebuild the channel BRAND is dissolving); (3) no stage produces
ComputationNode trees and no FunctionRef carrier is landed — call sites
have no v4 representation. Fix: T-9 BindsTo materialization lands as a
rider on #4581's binding_id stamping (same write, same seam), serving
the dependency classifier, structural_resolution lens, and this checker
with one producer. Slice step 2 now gated on that producer.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: sizing — COMPREP (function bodies in the v4 pipeline)

Measured: the THESIS computation substrate is consumable shapes with
zero producers — no stage builds ComputationNode trees, no FunctionRef
carrier landed, eval's Transform arm is a call_primitive slot, and the
mvp1 'emitted add fn' is a TypeNode Arrow signature (the T0/RTADD/T1
receipts are type-expr-tier). Sized as a first-class node: wave 0
carriers ride #4581 binding_id + the T-9 rider (no new FunctionRef
carrier, fewer variants; body = Arrow.body per E-9); wave 1 keystone =
source-ingested add body through parse/resolve/infer/eval by execution
(~PROV-sized); waves 2-4 behaviors/translate/breadth. Gates SELFHOST
facets 1-2 (co-equal with SPINE), termination-checker layer 3, emit
ladder T4+, STAGE-ADOPTION. Recommends honest relabeling of T0/RTADD/T1
as signature-tier in the dep graph. Cross-linked from the termination
design's prerequisite section.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: portfolio-review fixes — Node identity-channel authority + four seam closures

New: design-node-identity-channels.md — single P2 authority for Node-
carried fields and equality participation (binding_id IN / occurrence id
OUT / BindsTo rides the binding_id channel); #4581 is the linchpin seam;
landing order fixed; allocator-determinism obligation flagged to #4581
(DB-8/fixed-point back door). PROV Q-P2 resolved against it; COMPREP
wave 0 lands through it.

Seam closures: Map Q-M1 reconciled to canonical-order-is-representation
(insertion-order draft withdrawn; canonical total order on keys named as
the introduced requirement); map_get/match_pattern bridge deletion
ownership assigned to the Map landing with the Optional sweep explicitly
excluding the site (deep flavor => one co-landed PR); value-set
de-gated from the termination checker (structurally terminating;
checker validates it later, nothing waits).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: fix doc_refs CI (regen doc-chain) + resolve T3 dual-authority seam

- docs/thesis/doc-authority.md: regenerate embedded doc-chain via
  check_doc_refs.py --write-graph (new design docs joined the graph;
  the stale chain was the doc_refs CI failure).
- design-bidirectional-coercion.md §6: precedence note — rows-not-
  closures remains the direction authority; the T3 fold-carrier binding
  decision (incl. positional/labeled discipline) lands only after the
  one bounded run, with design-optional-surface.md §4 as the single
  authority for sequencing (review thread r3384485736).

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

---------

Co-authored-by: Claude <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Jun 10, 2026
…1/A.2)

Runtime architecture: pure total core (no panics by construction —
modeled refusal vs host fault, never collapsed); effects reified as
typed requests minted only against declared EffectSignatures (purity
structurally enforced, fail-closed at eval); handlers as extdeps/
runtimes bundles (pure/test, host via the one host_run door, dispatch);
arena-per-run store under P4; run-loop = bounded fold over the #4566
RunnableFrontier; dispatch-is-an-effect unifies Brief D as one handler;
answers D's five-question input spec inline. Co-keystone slice with
COMPREP wave 1 + an effects slice under the pure handler bundle.

Brand phase 2: mint-once at the declaring module keyed by QualifiedName;
imports reference and re-exports preserve binding_id through the
03_name_resolve Admission carrier (no spelling-joins at module
boundaries); corpus determinism decision escalated — canonicalized
allocation (rec) vs content-derived ids, touching in-flight #4581;
slice includes the cross-module A3 brand-twin rejection and an
order-perturbation determinism claim. Doc-chain regenerated.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4
@briansrls

Copy link
Copy Markdown
Contributor Author

Closing to avoid confusion — this PR implements the SUPERSEDED design. The brand-identity work was re-ratified to the binding_id approach in #4587 (Amendment 4) after codex proved the original Node.ident/ident_span approach unsound (an InternTable spelling-id is NOT declaration identity). This PR's code is still the old approach (16 with_authored_identity/ident_span-graft sites, zero binding_id), so it can never meet the undraft receipt matrix (you can't prove 'authority-direct binding_id' with code that has no binding_id). Rather than untangle, the binding_id implementation restarts fresh on the #4587 6-step contract (substrate BindingId/TypeDeclBinding/decl_registry → build_type_env registration → atomic ident_span-graft deletion + with_preserved_binding_id → PD-3 compares binding_id → dogfood → Amendment-4 guardrails) with the full by-execution receipt matrix (incl. the 11/11 adversarial PD-3 suite ported from #4536, brand-twins reject by execution, one origination site). No work is lost that the new design doesn't redo correctly; the #4536 verification + the #4587 design are the durable artifacts. — sent from still-raven-546

@briansrls briansrls closed this Jun 10, 2026

@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: 1c746198 · Trigger: schedule
  • Thinking: 437s wall

BLOCKING (1)

Root Cause

  • src/v2/04_types.dag Leaf declaration identity was modeled as a local compatibility check instead of the single leaf-type equality authority → route node_type_equals/core leaf cases through the same identity comparison.

⚠️ The identity channel is moving in the right direction, but one brand-erasing equality path remains.

Comment thread src/v2/04_types.dag
@@ -769,7 +780,7 @@ fn node_type_compatible(left: Node, right: Node, source_indices: Map<String, New
else { node_type_compatible(left: left_inner, right: right_inner, source_indices: source_indices) }

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.

Invariant violation: BLOCKING: Identity-aware leaf comparison is only wired into node_type_compatible; node_type_equals remains authored-name based for callers like src/v2/04_access.dag:88, so honest ident_span can collapse distinct brands and violates Facts Flow Forward.

@briansrls
briansrls deleted the session/eager-seal-256 branch June 10, 2026 02:15
briansrls added a commit that referenced this pull request Jun 10, 2026
… phase-2 designs (#4609)

* docs: compute-fabric design briefs A-D + PROV status flip

Four grounded designs for the compute fabric (the coercion flip applied
to provisioning), rebased onto merged #4605:

- design-compute-request.md (A): ComputeRequest as a typed fact-bundle —
  dimensioned interval resource asks, closed capability vocabulary with
  per-kind satisfaction rules, workload effect facts; lands only inside
  the A+B+C slice (no request type without its resolver).
- design-compute-providers.md (B): ComputeProvider concept in std/,
  homelab/gcp instances in extdeps/compute/; availability classes carry
  obligation sets discharged structurally against workload effect facts
  (Preemptible => re-runnable via the effects partition); declared-vs-
  reality divergence detected fail-closed at dispatch; unify-with-OaaS_v2
  argued over greenfield (P5). gunb.ai-side grounding marked out-of-clone.
- design-compute-policy-selection.md (C): compute_select as a
  find_witness domain wrapper (constraints.dag precedent) plugging into
  the existing MultiplicityPolicy/TargetDeclaredPriority seam; policy =
  declared lexicographic ordering over dimensioned objectives; ties and
  zero-satisfier cases refuse with a per-candidate located report; no
  fold variant added; A+B+C slice with 5 claims is prototypable now.
- design-compute-dispatch.md (D): gated dependency statement — OaaS_v2
  bridge contract with P2 host-boundary discipline (no implicit
  re-execution; re-selection is declared policy), dissolution trigger on
  the native runtime path, and the 5-question input spec the runtime-
  architecture design must answer for its first real consumer.

Also: design-provenance-span.md status flipped HELD -> dispatched
(operator GO 2026-06-09, #4592); doc-chain regenerated.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: v4 runtime-architecture + brand phase-2 designs (design-TODO A.1/A.2)

Runtime architecture: pure total core (no panics by construction —
modeled refusal vs host fault, never collapsed); effects reified as
typed requests minted only against declared EffectSignatures (purity
structurally enforced, fail-closed at eval); handlers as extdeps/
runtimes bundles (pure/test, host via the one host_run door, dispatch);
arena-per-run store under P4; run-loop = bounded fold over the #4566
RunnableFrontier; dispatch-is-an-effect unifies Brief D as one handler;
answers D's five-question input spec inline. Co-keystone slice with
COMPREP wave 1 + an effects slice under the pure handler bundle.

Brand phase 2: mint-once at the declaring module keyed by QualifiedName;
imports reference and re-exports preserve binding_id through the
03_name_resolve Admission carrier (no spelling-joins at module
boundaries); corpus determinism decision escalated — canonicalized
allocation (rec) vs content-derived ids, touching in-flight #4581;
slice includes the cross-module A3 brand-twin rejection and an
order-perturbation determinism claim. Doc-chain regenerated.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: review fixes — selection-seam overload removed, dispatch wait-bound made structural

r3384872268 (accepted): compute_select no longer overloads
TargetDeclaredPriority.priority with an ordering meaning — verified
find_witness_realized treats priority as an exact selected candidate
(identical routing to UserSelected), so the overload would give one
carrier two type-indistinguishable meanings (P2). The ordering is now a
compute-domain ComputePolicy carrier; the wrapper computes the
lexicographic argmax (ties refuse) and invokes find_witness with
UserSelected{argmax}; find_witness carriers untouched.

r3384872272 (accepted): an unbounded compute ask can no longer reach a
waiting handler — the dispatch effect-request constructor structurally
requires the finite wait-bound fact (same constructor-requires-fact
pattern as effect signatures); P4 bounded waiting enforced at the
boundary that waits, not by policy goodwill.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: review fix — capacity satisfaction tests the hard minimum, grant carried in SelectionResult

r3385120097 (accepted): the capacity clause required provider containment
of the whole requested interval, but the interval's upper end is
max-useful (allocation preference), not a requirement — containment would
refuse providers that satisfy the ask (P1 modal-force compression).
Fix per the review's option (b): satisfaction = provider.available >=
request.min per dimension; the granted allocation
min(available, max_useful) is computed at selection and carried in
SelectionResult (the dispatcher needs the grant anyway); preferring
larger grants is available to policies as an objective, separated from
satisfaction. Request doc now states the two ends' modal force at the
type.

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

* docs: align §2 grounding row with the min-satisfaction capacity fix (r3385120097 residue)

https://claude.ai/code/session_018QC433THjRyqiHuP8czPi4

---------

Co-authored-by: Claude <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