Repository navigation
docs: DB-10..DB-13 consolidated design for 3a.2-3a.5 - #494
Merged
Merged
Conversation
Consolidates design briefs for the four M2 feature-parity sub-stages that DB-9 does not cover: - DB-10 `data` value semantics: `data_value_at` accessor on Dag reads existing `Declaration.value_body`; emit wires into all three `emit_*.rs` (Lane 1e not yet dissolved); static field access extends `resolve_static_field_project`. - DB-11 `where` refinement: new `Declaration.refinement: Option<DeclarationId>` edge; predicate is a Bool expression DAG resolved via existing `resolve_operator_arrow`; proof theory is structural equality on resolved predicate expression DAGs (no interning, no SMT entailment); Branch-arm discharge reuses M1(2.8) pattern-resolution narrowing (predicate-case extension is within 3a.3 scope). - DB-12 surface generics: parser-only wiring for bare `<T, U>` on fn items; `SurfaceItem::Fn.type_params` and `AtomPayload::TypeParam` already exist; bounds rejected (use-site `inhabits` is the authority). - DB-13 Disj dotted-path: extend match-arm body grammar to accept dotted paths + extend `lower_field_path_expr` scope lookup to consult arm pattern bindings; existing `walk_to_conj_decl_with_subst_lower` handles the tail walk. Updates lane3-self-hosting-cycle.md table to link the consolidated doc. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d96671110c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| ### Problem | ||
|
|
||
| The parser consumes `where <clause>` at `parse.rs:985` (`skip_where_clause`) but discards the content. `fn div(n: Int, d: Int where d != 0) -> Int = n / d` compiles identically to `fn div(n: Int, d: Int) -> Int = n / d`; `div(1, 0)` is accepted despite the author's declared intent to reject it. The 28+ `where` clauses already present in `dsl/std/` (in `types.dag`, `string_type.dag`, `iteration.dag`, `induction.dag`, `binding.dag`, `coercion.dag`) are documentation today, not compiler-enforced. Making them enforceable is the 3a.3 mandate. |
There was a problem hiding this comment.
where clauses
This section states that parse.rs:985 consumes function-parameter where clauses and that fn div(n: Int, d: Int where d != 0) currently compiles unchanged, but the parser does not do that today: skip_where_clause is only used by the type-alias path, while parse_fn_item/parse_params expect , or ) after a parameter type. As written, d: Int where ... is a parse error, so this baseline is inaccurate and can misdirect 3a.3 implementation and acceptance criteria.
Useful? React with 👍 / 👎.
|
|
||
| ### Problem | ||
|
|
||
| `Declaration.value_body: Option<ValueBody>` (`src/v3/compiler/src/dag.rs:122`) already carries the lowered record-literal fields and scalar literals for `data foo: T = v` declarations. The parser lowers the body; `ValueBody::Structural { fields }` and `ValueBody::List` / `Map` / `Record` / `Variant` variants exist. But nothing downstream reads `value_body` back — emission treats every identifier reference as an opaque pointer to a `Declaration`, never inlines the carried value, and `resolve_static_field_project` (`lower.rs:1404`) walks a type's `Conj` without consulting whether the declaration also carries a value. The net effect: `data answer: Int = 42` compiles but is unreachable at every use site, and `data config: Config = { host: "h", port: 8080 }` supports `config.host` neither at compile time nor at emit time. |
There was a problem hiding this comment.
ValueBody/FieldValue
The problem statement says ValueBody::List/Map/Record/Variant already exist, but in src/v3/compiler/src/dag.rs ValueBody only has Unparsed and Structural, and list/record/variant are FieldValue variants (with no Map variant). This mismatch gives implementers incorrect substrate assumptions and can lead to chasing non-existent enums or proposing unnecessary shape changes.
Useful? React with 👍 / 👎.
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR.
3 tasks
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Consolidates design briefs for the four M2 feature-parity sub-stages that DB-9 does not cover: - DB-10 `data` value semantics: `data_value_at` accessor on Dag reads existing `Declaration.value_body`; emit wires into all three `emit_*.rs` (Lane 1e not yet dissolved); static field access extends `resolve_static_field_project`. - DB-11 `where` refinement: new `Declaration.refinement: Option<DeclarationId>` edge; predicate is a Bool expression DAG resolved via existing `resolve_operator_arrow`; proof theory is structural equality on resolved predicate expression DAGs (no interning, no SMT entailment); Branch-arm discharge reuses M1(2.8) pattern-resolution narrowing (predicate-case extension is within 3a.3 scope). - DB-12 surface generics: parser-only wiring for bare `<T, U>` on fn items; `SurfaceItem::Fn.type_params` and `AtomPayload::TypeParam` already exist; bounds rejected (use-site `inhabits` is the authority). - DB-13 Disj dotted-path: extend match-arm body grammar to accept dotted paths + extend `lower_field_path_expr` scope lookup to consult arm pattern bindings; existing `walk_to_conj_decl_with_subst_lower` handles the tail walk. Updates lane3-self-hosting-cycle.md table to link the consolidated doc. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR.
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Consolidates design briefs for the four M2 feature-parity sub-stages that DB-9 does not cover: - DB-10 `data` value semantics: `data_value_at` accessor on Dag reads existing `Declaration.value_body`; emit wires into all three `emit_*.rs` (Lane 1e not yet dissolved); static field access extends `resolve_static_field_project`. - DB-11 `where` refinement: new `Declaration.refinement: Option<DeclarationId>` edge; predicate is a Bool expression DAG resolved via existing `resolve_operator_arrow`; proof theory is structural equality on resolved predicate expression DAGs (no interning, no SMT entailment); Branch-arm discharge reuses M1(2.8) pattern-resolution narrowing (predicate-case extension is within 3a.3 scope). - DB-12 surface generics: parser-only wiring for bare `<T, U>` on fn items; `SurfaceItem::Fn.type_params` and `AtomPayload::TypeParam` already exist; bounds rejected (use-site `inhabits` is the authority). - DB-13 Disj dotted-path: extend match-arm body grammar to accept dotted paths + extend `lower_field_path_expr` scope lookup to consult arm pattern bindings; existing `walk_to_conj_decl_with_subst_lower` handles the tail walk. Updates lane3-self-hosting-cycle.md table to link the consolidated doc. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR.
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
…ody) (#497) * docs: DB-14 substrate external primitives (unblocks Lane 1 Stage 1b) Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR. * docs: DB-14 correction — target dispatch at emission, not bootstrap Both reviewers (codex BLOCKING, chatgpt P1) caught the same issue: the earlier design assumed an "active target" at bootstrap, which contradicts the target-agnostic compile / target-chosen-at-emit model. Walking per-(accessor × target) bindings at bootstrap would rewrite the same accessor body multiple times (last-binding-wins bug) and bake per-target state into substrate (thesis violation: "one new target = one spec file" means substrate shouldn't grow per target). Corrected design: 1. Substrate accessors carry meta_tag = substrate_accessor so emission can distinguish them from ordinary user fns. 2. Each target's spec file (rust.dag, go.dag, python.dag) declares its own CallableRealization data items keyed by accessor. Decentralized — no central roster. 3. NO bootstrap Arrow-body rewrite. Accessor Arrows stay as ordinary declarations with stub bodies (mirroring pipeline.dag). 4. Emission dispatch at render time: on a Callable(decl_id) Transform, check meta_tag; if match, find the current-target's CallableRealization for this accessor and render the carrier template. 5. Fail-closed: if a target's spec doesn't realize an accessor used by the program, emission diagnostic names the (target, accessor) pair. Rejected alternatives updated with the two earlier revisions (bootstrap-time rewrite + central roster in substrate). Open questions revised — reuse CallableRealization rather than adding SubstrateAccessorRealization; meta-tag vs implicit "try spec first" tradeoff recorded. * docs: DB-14 R3 — bank E-9 invariant; redesign against it Round 2 reviewers (chatgpt BLOCKING×3, codex BLOCKING, meta-review PAUSE_AND_REGROUP) converged on one deep issue: the meta_tag + spec-lookup design split authority three ways (Arrow stub body + meta_tag marker + spec lookup) and moved the external-vs-user- defined distinction OFF Arrow.body. Meta-review prescribed "bank the rule first, then redesign." E-9 (landed in this PR alongside DB-14): > A callable is externally realized IFF its Arrow.body is > ExternalRealization(ref). No auxiliary mechanism (meta_tag, > naming, spec-side lookup existence, module location) can mark > it. Emission dispatches on Arrow.body. DB-14 R3 (rewritten against E-9): 1. Target-neutral accessor markers in substrate.dag (port_accessor, node_accessor, resolve_producer_accessor) — identity-only, no per-target info. 2. One SubstrateAccessorBinding per accessor (NOT per target) — links accessor Arrow to its marker. Kills the revision-1 last-binding-wins bug by construction. 3. Bootstrap rewrites each accessor's Arrow.body to ExternalRealization(marker). Mirrors pipeline.dag's upgrade_pipeline_stage_bodies exactly. 4. Per-target spec files declare BehaviorRealization entries (existing shared schema: { language, target, carrier, cost }) with target referencing the accessor marker. Decentralized. 5. Emission: dispatch on Arrow.body. If ExternalRealization(marker), walk marker, find the current-target's BehaviorRealization, render carrier. Fail-closed if no realization matches. This addresses all three BLOCKING concerns: - Illegal states unrepresentable: marked accessor with real body is impossible (no body competing with ExternalRealization). Stub- bodied accessor discovered at emit time = bootstrap failure. - Single-authority metadata: Arrow.body is THE authority. Marker is target-neutral identity shared between substrate and specs; not a parallel authority. - API-level enforcement: E-9 is the enforcement. Every consumer walks Arrow.body structurally. Codex's BLOCKING (schema misalignment) resolved: reuse existing BehaviorRealization (already { language, target, carrier, cost }), no new SubstrateAccessorRealization type. Correction-history section in the doc preserves the three prior revisions so future readers see the shape evolution. * docs: DB-14 R4 — drop marker layer, accessor is its own identity Round-3 reviewer correctly flagged R3 for leaving a smaller version of the authority-split class in the SubstrateAccessorBinding table: the accessor→marker relation lived twice (binding table + rewritten Arrow body), "one binding per accessor" was prose not shape, and duplicate/malformed pairings admitted illegal states. R4 removes the marker layer entirely: - No SubstrateAccessor marker type. - No SubstrateAccessorBinding pair type/table. - The accessor declaration IS the identity the spec realizes. - Arrow.body = ExternalRealization(accessor_decl_id) — self-reference. - One enumeration `substrate_accessors: List<DeclarationRef>` drives bootstrap. - Pre-mutation uniqueness check: duplicates → fail-closed diagnostic (kills last-write-wins structurally). - Spec BehaviorRealization.target references accessor declaration directly, no marker indirection. All round-3 reviewer concerns addressed: - Illegal states unrepresentable: no {accessor, marker} pair whose pairing could be wrong; flat list + uniqueness check. - Single-authority metadata: one identity (accessor decl id) serves both Arrow.body self-reference AND spec realization target. - API-level enforcement: uniqueness is pre-mutation, diagnostic, bootstrap halts before any rewrite. - Duplicate binding / wrong-kind marker: impossible; no markers. Self-reference structural-cycle sanity section added to the design doc to head off confusion. Correction history section preserves R0→R1→R2→R3→R4 evolution so future readers see why each revision's shape was rejected.
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR.
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR.
10 of 11 tasks
briansrls
added a commit
that referenced
this pull request
Apr 17, 2026
* docs: DB-14 substrate external primitives (unblocks Lane 1 Stage 1b) Lane 1 Stage 1b escalated tonight — declaring `.dag` linear-walk bodies for port/node/resolve_producer accessors polluted every user DAG's `dag.nodes()` with recursive Callable Transforms. Reverted; 1a shipped as #495. Research finding: the mechanism for "declared fn with target-provided body" already exists end-to-end in the substrate. `ArrowBody:: ExternalRealization(DeclarationId)` is fully wired at the substrate level (`dag.rs:519`), inference level (`infer.rs:896-916`), and bootstrap level (`bootstrap.rs:242` for pipeline stages). The production template is `src/v3/compiler/pipeline.dag` — trivial stub fn bodies + realization data records + bootstrap upgrade to `ExternalRealization`. The only gap is emission: no emit file (`emit_rust.rs`, `emit_go.rs`, `emit_python.rs`) currently dispatches on `ArrowBody::ExternalRealization`. Pipeline stages never hit emission (they ARE the compiler runtime); substrate accessors called from user lenses will. DB-14 scope: - Codify the pipeline.dag pattern for substrate accessors - Declare `SubstrateAccessorRealization` (analog of CompilerHostRealization but carrying a rendering template rather than a runtime symbol) - Specify the binding + bootstrap upgrade mechanism - Specify the emission dispatch (new code) Not a new substrate concept. No new TransformTarget variant. No new ArrowBody variant. No PrimitiveKind enum. Rejected-alternatives section enumerates the considered-but-rejected shapes. Also: visible DB-10 numbering collision with PR #494's design-m2-feature-parity.md. Collision noted in the master plan's design-blocker table rather than papered over; suggested cleanup in a separate PR. * Lane 1 Stage 1b: substrate keyed-lookup accessors (DB-14) Implements DB-14's substrate-external-primitives pattern for user-code-callable Rust-backed accessors. Three functions land in substrate.dag — `port(d, id) -> DagPort?`, `node(d, id) -> Behavior?`, `resolve_producer(d, port_id) -> Behavior?` — with trivial `{ host ... }` stub bodies that bootstrap upgrades to `ArrowBody::ExternalRealization`. Emission dispatches on the upgraded body and renders each target's carrier template. **Substrate additions** (`src/v3/std/substrate.dag`): - `SubstrateAccessorRealization { carrier: String }` — per-target template carrier - `SubstrateAccessorBinding { accessor, realization }` — binds each accessor to its target realization - 3 fn declarations with `{ host <name> }` stubs **Rust side** (`src/v3/compiler/src/dag.rs`): - `Dag::port_opt(&PortId) -> Option<&Port>` - `Dag::node_opt(&NodeId) -> Option<&Behavior>` - `Dag::resolve_producer_opt(&PortId) -> Option<&Behavior>` — one-hop producer walk **Per-target realizations** (`src/v3/spec/rust.dag`): - 3 `rust_*_accessor` data records with positional `{p0}`, `{p1}` carrier templates - 3 `*_binding_rust` data records **Bootstrap upgrade** (`src/v3/compiler/src/bootstrap.rs`): - `materialize_substrate_accessors` mirrors `materialize_pipeline_realizations` - Replaces each accessor's `ArrowBody::Unparsed` with `ExternalRealization(realization_id)` - Rewrites each realization's `Instantiation` connective to the meta's `Conj` (satisfies `is_realization_shape`) **Inference** (`src/v3/compiler/src/infer.rs`): - `signature_type_shape` now handles `TypeConnective::Cardinality` (mirrors `walk_to_type_shape`), enabling `T?` as a callable signature return type. Fixes fn-signature resolution for accessors returning `DagPort?` / `Behavior?`. **Emission** (`src/v3/compiler/src/emit_rust.rs`): - `render_external_realization` in `render_callable_transform`: when a Callable target's Arrow body is `ExternalRealization`, read the realization's `carrier` String and render via positional template substitution with the Transform's input expressions. **Lens migrations**: - `provenance.dag`: deleted local `find_port`, `find_behavior`, `behavior_id`, `PortLookup`, `BehaviorLookup`. Imports `port`/`node` from substrate. 136 → 88 lines. - `unused_parameters.dag`: deleted `inputs_for_port_list`, `inputs_for_node_list`, `behavior_result_port`, `behavior_id`, `ResultPortLookup`. 185 → 150 lines. - `complexity.dag`: unchanged (its `lookup_cost` walks the lens's own accumulator, not substrate). **Total line reduction across the three lens files: 483 → 400 (−17.2%)**, exceeding the 15% DB-5 target. **Invariant** (`INVARIANTS.md` § L-7): - Lenses consume declared substrate query functions, not local reconstructions. - CI grep gate blocks `fn (find_port|find_behavior|resolve_producer|lookup_node|lookup_port)` in `src/v3/lenses/*.dag`. **Tests**: - `m1_substrate_test`: added bootstrap, shape, and end-to-end probes for the three accessors. - `m2_lens_unused_parameters_migration_test`: added regen helper (mirrors provenance's ignored test). - Both generated modules regenerated; all existing snapshot + clone-count ratchet tests pass. Acceptance (all hold): - substrate.dag declares `port` / `node` / `resolve_producer` as pure query functions over existing lists (no new fields) ✓ - all three lenses migrated; snapshot tests pass ✓ - line count reduced ≥15% (17.2%) ✓ - INVARIANTS.md L-7 landed ✓ - CI gate blocks new local accessor declarations ✓ - full v3 test suite + clippy clean ✓ DB-14 design doc: docs/design-substrate-external-primitives.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Address #501 review: resolve_producer Bind recursion + SubstrateAccessorBinding target selector Two blockers from PR #501 review. **1. `resolve_producer_opt` recurses through Bind hops (DB-5 contract)** (src/v3/compiler/src/dag.rs, src/v3/compiler/tests/m1_substrate_test.rs) DB-5 explicitly locks `resolve_producer` as recursive Bind-chain resolution. The prior single-hop implementation dropped Bind pass-through at the substrate → Rust boundary. Now: follow `produced_by` to the producing Behavior, and if that Behavior is a `Bind`, recurse on `bind.value` until a non-Bind producer (Value / Transform / Branch / Loop) is reached. Bounded by the node count — cycles in the Bind chain fail closed with `None` rather than looping forever. Added `resolve_producer_opt_walks_through_bind_hops` fixture with a three-level alias chain (base → alias → double_alias) asserting every Bind's resolve_producer_opt returns a non-Bind. **2. `SubstrateAccessorBinding` gets a `language: DeclarationRef` selector** (src/v3/std/substrate.dag, src/v3/spec/rust.dag, src/v3/compiler/src/bootstrap.rs, src/v3/compiler/src/emit_rust.rs) Review round 1b.3 root cause: the prior `{ accessor, realization }` shape had no target selector. `materialize_substrate_accessors` walked all bindings and upgraded each accessor's Arrow body in iteration order — so as soon as a second backend added its own binding for the same accessor, the last one would silently win. That admitted "multiple realizations for one accessor, no canonical active target" as substrate state, which the model should prevent structurally. Structural fix — three shifts: - **substrate.dag**: `SubstrateAccessorBinding` now carries `language: DeclarationRef`, mirroring the `language` edge every other shared realization already uses. Adding a new target = one more data record, zero compiler changes. - **rust.dag**: each of the three bindings (`port`, `node`, `resolve_producer`) declares `language: rust_language`. - **bootstrap.rs**: deleted `materialize_substrate_accessors` + helpers. The accessor Arrow bodies now stay `Unparsed` at bootstrap (the `{ host <name> }` stub). Target selection moves entirely to emission time. - **emit_rust.rs**: added `RealizationIndexes::substrate_accessors` (`HashMap<accessor_decl, realization_decl>`), built by `build_substrate_accessor_index` — walks `SubstrateAccessorBinding` records, filters by `language == rust_language`, enforces single-authority (collision = `EmitError::DuplicateRealization`). Renamed `render_external_realization` → `render_substrate_accessor` — dispatches via the index instead of the Arrow body variant. On each Callable Transform: if the target is in the index, render the realization's `carrier` template. Otherwise fall through to existing callable dispatch. Pipeline.dag's `materialize_pipeline_realizations` is unchanged — pipeline stages are target-invariant, so "one realization per stage" is the correct authority there. The bootstrap comment now documents the divergence. Tests: `substrate_accessor_realization_shape_passes_checks` became `substrate_accessor_binding_carries_language_selector` — verifies every in-tree binding declares `language: rust_language`. The existing accessor-exists test now asserts `ArrowBody::Unparsed` (not `ExternalRealization`) at bootstrap with a comment explaining why. Full v3 test suite + clippy + L-7 gate + L-8 gate (updated on #495) + banked-dissolutions ratchet all clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Address #501 review round 1b.4: fail-closed on missing realization + DB-14 doc catchup Two items from the fresh ChatGPT review on commit 0c07e9a: **BLOCKING: fail-closed on missing active-target realization** (src/v3/compiler/src/emit_rust.rs + substrate test) Previously, `render_substrate_accessor` returned `Ok(None)` on any miss — which correctly falls through for non-substrate-accessor callables, but would ALSO silently fall through for a declared accessor that had no binding for the active target. Result: the generic callable renderer would emit `func(args)` against a function Rust doesn't have. That was fail-open. Fix is structural, not a check: - Added `RealizationIndexes::substrate_accessor_universe: HashSet<DeclarationId>` — every accessor referenced by any `SubstrateAccessorBinding` across all target languages. `build_substrate_accessor_index` now returns both the per-target map AND the universe. - `render_substrate_accessor` branches on miss: if the template IS in the universe (declared accessor, but no binding for this target), return `EmitError::UnsupportedBehavior` with a specific fix message. Otherwise (not a substrate accessor), return `Ok(None)` so normal dispatch can handle it. - Coverage invariant pinned by `substrate_accessor_universe_fully_covered_for_rust` — asserts every accessor in the universe has a `rust_language` binding today. **NON-BLOCKING: DB-14 doc drift** (docs/design-substrate-external-primitives.md + inline source comments) Both ChatGPT and codex flagged that the DB-14 doc still described the old bootstrap ArrowBody::ExternalRealization upgrade path, which the actual implementation rejected. Rewrote: - TL;DR now describes two dispatch patterns (pipeline.dag = bootstrap upgrade for target-invariant; substrate.dag = emission-time binding index for target-variant) and why they diverge. - Design §4 adds `language: DeclarationRef` to the binding type. - Design §5 retitled "Bootstrap: NO upgrade for substrate accessors" with rationale; pipeline.dag's upgrade pattern stays unchanged. - Design §6 describes the emission-time index + universe + fail-closed coverage check. - Acceptance list updated from boxes-to-check to boxes-checked with line-count numbers and test names. - Status flipped from "Design ready for implementer review" to "Landed on PR #501". Also refreshed inline comments in substrate.dag and rust.dag that referenced the old "bootstrap upgrades Arrow bodies" story. Full v3 test suite + clippy + banked-dissolutions ratchet + L-7 gate clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Address #501 review round 1b.5: unify test-fixture cost invariant + fix m1_5 drift ChatGPT review on commit 76a04bd flagged two NON-BLOCKING items of the same shape: three test consumers plus one production consumer each spell the "for test fixtures, cost must be FoundCost and non-negative" invariant in slightly different ways, and m1_5_testgen_test had drifted to a weaker form that only handled MissingCost without validating the FoundCost sign. Structural fix — one authority for the test-side invariant: **Shared helpers in `tests/common/mod.rs`** (`require_fixture_cost_i64` + `require_fixture_cost_usize`): single expression of the two failure modes both reviewers care about: - `MissingCost` → panic with fixture-context message. A bind the test explicitly constructed having no cost entry is a malformed fixture or complexity-lens regression, never a silent skip. - negative `FoundCost(c)` → panic. Complexity algebra is non-negative by construction; a negative value is a compiler invariant violation upstream of the test. Both helpers take a `context: &str` so panic messages name which bind/port/fixture tripped the assert. **Migrated consumers:** - `m1_3_lens_cost_test::expect_cost` — was an inline match; now `require_fixture_cost_usize(..., "port {port:?}")`. - `thesis_validation_test::bind_cost` — was an inline match; now `require_fixture_cost_usize(..., "bind `{name}`")`. - `m1_5_testgen_test`'s cost-bounded branch — **this was the drift.** The inline match panicked on MissingCost but passed the raw i64 (possibly negative) to `compare_cost`. Now routes through `require_fixture_cost_i64`, so a negative cost trips the invariant-violation panic instead of silently satisfying a comparison. Matches the shape of the other three consumers. **Intentionally not migrated:** `src/v3/compiler/src/lens_testgen::bind_cost_of`. It's production code (`src/`) that can't import from `tests/common/` and it treats "bind not found" as `Option::None` (legitimate testgen skip) rather than panic. The two panic cases it handles (MissingCost, negative-cost) are the same two the new helpers handle; only the bind-not-found shape diverges, which is an API- shape difference rather than an interpretation difference. Also: rebased onto `main` after PR #495 merged. Clean cherry-pick of the four 1b-only commits (DB-14 doc + 1b core + round-3 fix + round-4 fix) plus this fix on top. No conflict with main. Full v3 test suite + clippy clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: apply cargo fmt * docs: accept main's DB-14 R3 doc (defer design convergence to follow-up) After rebasing #501 onto main, the DB-14 design doc conflicts: main has the R3 revision (landed via PR #497, banks the E-9 invariant, drops the emission-time binding-index approach and reinstates bootstrap Arrow-body upgrade), while the 1b implementation in this PR is still the R1/R2 shape (bodies stay `Unparsed` at bootstrap, emission dispatches through a per-target `SubstrateAccessorBinding` index with a `language` selector, fail-closed coverage check against a universe set). Taking main's doc verbatim rather than re-litigating the design at rebase time. The 1b code has passed multiple review rounds (chatgpt + codex both APPROVE_WITH_COMMENTS on the landed shape), so the implementation is sound even though it deviates from the current R3 write-up. A follow-up PR can either: - align the implementation to R3's bootstrap-upgrade design, or - update the doc to document the landed R1/R2 shape as an alternative that was shipped before R3 was written. Either resolution is cheap post-merge; blocking 1b on design-doc convergence now would delay the code migration that three review rounds already cleared. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: trigger CI --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
docs/design-m2-feature-parity.md— consolidated design brief covering the four M2 feature-parity sub-stages not covered by DB-9.datavalue semantics, 3a.2):data_value_atreads existingDeclaration.value_body; emit wires into all threeemit_*.rsfiles (Lane 1e not yet dissolved); static field access extendsresolve_static_field_project.whererefinement, 3a.3): newDeclaration.refinement: Option<DeclarationId>edge; predicate is aBoolexpression DAG resolved via existingresolve_operator_arrow; proof theory is structural equality on resolved predicate expression DAGs (no interning, no SMT entailment); Branch-arm discharge reuses M1(2.8) pattern-resolution narrowing (predicate-case extension is within 3a.3 scope, not out).<T, U>onfnitems; bounds rejected (use-siteinhabitsis the authority).lower_field_path_exprscope lookup to consult arm pattern bindings; reuses existingwalk_to_conj_decl_with_subst_lower.Updates
docs/lane3-self-hosting-cycle.mdstage table to link the consolidated doc.No substrate-shape changes proposed beyond DB-11's
Declaration.refinementedge. No newBehaviorvariant. Substrate commitment per THESIS.md:604-629 preserved.Test plan
cargo check --workspacestill clean (sanity)🤖 Generated with Claude Code