Repository navigation
v3: implement substrate reflection prereqs 1 and 2 - #458
Conversation
Replace expression-position local dotted paths with structural `TransformTarget::FieldProject { parent_type, field_label }` nodes. Lowering now emits one projection Transform per segment, inference resolves the projected field type directly from the parent Conj, and emit_rust renders the projection as `.field` without synthesizing accessor declarations.
§9 receipt: extend the Transform target coproduct, not Behavior and not the declaration table. Field access is a dispatch target carried by Transform itself; this commit does not add synthesized accessor Declarations, parallel metadata, or surface-IR carry-through.
§8.10 4-pattern check: Pattern 1 fails because the projection fact has no other natural home; Pattern 2 fails because Callable, FieldProject, and Operator carry different payloads; Pattern 3 fails because projection is intrinsic structural elimination, not an algebra field; Pattern 4 fails because the dispatch targets are categorically distinct. Verdict: FieldProject is terminal at current scope.
Validation: cargo test -p v3-compiler; cargo clippy -p v3-compiler --all-targets -- -D warnings
Add `SurfacePattern::VariantWith { name, binding, span }` to the parser, add `PayloadBinding { binding_name, payload_port }` plus `Path.binding: Option<PayloadBinding>` to the substrate, and lower single-positional variant payload captures into typed arm-local ports.
BranchPattern stays at its existing two variants. Discrimination remains on `path.pattern`; extraction lives on `path.binding`. Lowering resolves the matched variant against the scrutinee Disj, allocates the payload port, inserts the binding name into the arm-local scope, and leaves inference decoupled from the binding record.
`binding_name` is carry-forward surface information for lowering scope insertion and readable emission; inference consumes `payload_port` and does not consult the name.
Validation: cargo test -p v3-compiler; cargo clippy -p v3-compiler --all-targets -- -D warnings
ChatGPT ReviewPrinciple audit. FAIL-CLOSED. Mostly satisfies, but behaviorally. New user-path failures become diagnostics, not silent drops: ILLEGAL STATES UNREPRESENTABLE. Does not satisfy; this is structural. FACTS FLOW FORWARD. Fails, and this is the deepest concrete bug. Payload binding is the good half: lowering turns the matched payload into a typed port and the arm body consumes that port ( COPROD DISSOLUTION. Fails. SINGLE AUTHORITY. Fails structurally. Field projection now has multiple competing authorities: the input port’s resolved type, the duplicated API-LEVEL ENFORCEMENT. Fails. Nothing in the substrate types prevents constructing an inconsistent Design question. Is field access in v3 a terminal computation-target Verdict. REQUEST_CHANGES. The direction is right—this round adds real user-facing capability and real substrate tests instead of more inert scaffolding—but the LOOP HEALTH: 📉 ACCUMULATING_DEBT — this round does enable real consumer tests, but it also adds a new scaffold ( |
![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: bb6e4207cf
ℹ️ 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".
| let Some(scrutinee_decl_id) = (match dag.port(scrutinee_port).state() { | ||
| PortState::Resolved(ty) => Some(ty.declaration), | ||
| PortState::Unresolved | PortState::Uninferred => None, | ||
| }) else { | ||
| dag.mark_unresolved( |
There was a problem hiding this comment.
lower_payload_binding immediately fails when the scrutinee port is Uninferred, but lowering runs before inference and many valid scrutinees (for example SurfaceExpr::Call and operator expressions) are created with untyped output ports and only resolved later. This makes valid payload matches like match id(x) { Some(v) => ... } fail closed purely due to phase ordering, even though the infer pass can resolve the scrutinee to a Disj afterward.
Useful? React with 👍 / 👎.
| }, | ||
| ); | ||
| }; | ||
| let Some(output_ty) = walk_to_type_shape(dag, field_decl_id, &SubstStack::new(), 0) else { |
There was a problem hiding this comment.
decide_field_project computes the projected field type with walk_to_type_shape(..., &SubstStack::new(), ...), which drops any instantiation context from parent_type. For generic records (e.g., Box<Int> with field type T), this either fails (TypeParam lookup has no substitution) or yields an unsubstituted type, so valid projections like b.value cannot type-resolve correctly.
Useful? React with 👍 / 👎.
| match declaration_to_port_shape(payload_type_decl, dag, span) { | ||
| Ok(ty) => dag.set_port_type(payload_port, ty), |
There was a problem hiding this comment.
Payload bindings take payload_type_decl directly from the variant template and pass it to declaration_to_port_shape without substituting the scrutinee’s instantiated arguments. On instantiated sums like Maybe<Int>, the bound variable gets the template TypeParam id instead of Int, which then causes downstream branch-arm type mismatches in otherwise valid matches.
Useful? React with 👍 / 👎.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · bb6e4207
BLOCKING (2)
Root Cause
src/v3/compiler/src/lower.rsBoth prerequisites resolve user-visible structure from PortState during lowering instead of carrying unresolved projection/payload facts into infer, which duplicates type authority via FieldProject.parent_type and makes valid programs fail before the fixpoint can type them -> move both resolutions behind infer and derive them from the input port or resolved branch variant.
Non-blocking — Strengths
src/v3/compiler/src/dag.rsTransformTarget::FieldProject lands with an explicit lifecycle receipt, so the new enum arm respects the coproduct-dissolution ratchet.src/v3/compiler/tests/m1_substrate_test.rsThe tests cover both success cases and fail-closed rejection paths for each prerequisite, which is the right regression surface for substrate work.
| }, | ||
| ) | ||
| } | ||
| PortState::Uninferred => { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| ) -> PayloadBinding { | ||
| let payload_port = dag.alloc_port(None); | ||
| let Some(scrutinee_decl_id) = (match dag.port(scrutinee_port).state() { | ||
| PortState::Resolved(ty) => Some(ty.declaration), |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
BLOCKING (2) Root Cause
Non-blocking — Strengths
|
Three coherence edits now that prereq implementations are in flight: 1. §11 Prereq 1 checklist — removed stale "delete substrate.dag FieldAccessor marker" item (§3.6 1a never adds FieldAccessor, so there's nothing to delete). Added infer.rs decide_field_project and multi-hop test items to match #458's actual implementation. 2. §11 Prereq 3 checklist — added call-site rewrite item, unannotated fail-closed test, and a scope note documenting the contextual-first landing (#457's intentional scope: lambdas lower only when an expected function type is available). Callback-rule lens test moved to follow-up scope. 3. inference-as-data-experiments.md §6 Q6 — replaced placeholder with I0 result summary and cross-reference to docs/inference-as-data-i0-result.md (ships with #457). Updated §7 "When this doc updates" to mark I0 as complete. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Three coherence edits now that prereq implementations are in flight: 1. §11 Prereq 1 checklist — removed stale "delete substrate.dag FieldAccessor marker" item (§3.6 1a never adds FieldAccessor, so there's nothing to delete). Added infer.rs decide_field_project and multi-hop test items to match #458's actual implementation. 2. §11 Prereq 3 checklist — added call-site rewrite item, unannotated fail-closed test, and a scope note documenting the contextual-first landing (#457's intentional scope: lambdas lower only when an expected function type is available). Callback-rule lens test moved to follow-up scope. 3. inference-as-data-experiments.md §6 Q6 — replaced placeholder with I0 result summary and cross-reference to docs/inference-as-data-i0-result.md (ships with #457). Updated §7 "When this doc updates" to mark I0 as complete. Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
ChatGPT ReviewPrinciple audit. FAIL-CLOSED. Mostly satisfies, behaviorally. The new explicit failure paths all go through diagnostics: dotted-path lowering fails closed on empty/nonlocal/uninferred/non-Conj/missing-field cases in ILLEGAL STATES UNREPRESENTABLE. Violates, structurally, and this is BLOCKING. FACTS FLOW FORWARD. Violates, structurally, and BLOCKING. For COPRODUCT DISSOLUTION. On the changed terminal/substrate choice, this round is better than the prior one. I would not block The remaining caveat is SINGLE AUTHORITY. Violates, structurally, and BLOCKING. API-LEVEL ENFORCEMENT. Violates, structurally, and BLOCKING. Nothing in the API prevents constructing Design question. Is Verdict. REQUEST_CHANGES. The direction is better than the earlier attempts: this diff avoids synthesized accessor declarations, and I would not re-raise the old algebraic-form objection to LOOP HEALTH: 📉 ACCUMULATING_DEBT — this round fixes some earlier shape mistakes, but it still lands new substrate semantics as tests-only metadata and grows a fresh emitter-side special case before the semantic boundary is settled. |
Meta-Review (Loop Health)Loop summaryFrom the attached artifacts, I can verify 3 recorded review rounds against 1 visible diff snapshot: 1 codex-cli review and 2 chatgpt-browser entries, spanning about 33 minutes from 2026-04-15 22:17Z to 22:50Z. The supplied files do not expose the full PR commit count, so I cannot verify total commits beyond the single current diff state in Forward progress evidenceThis loop is not pure churn. The current diff does enable real consumers:
That matters. The roadmap explicitly says a type or substrate shape with zero consumers is a paper exercise, not structural proof ( Debt accumulation evidenceThe loop is still shifting debt faster than it is paying it down. First, the same root cause is being rediscovered instead of dissolved. The browser review says lowering resolves the concrete Second, the diff adds fresh scaffold / invalid-state surface area:
Those shapes admit ambiguous or illegal combinations instead of making them unrepresentable ( Third, this recurring class has already been graduated in the project foundations, and the PR is still violating it. Fourth, the scaffold accounting is incomplete. Cheating signalYes, but documented. The implementer is not hiding compromises. But the most recent fixes are still small-blast-radius fixes: add tests, add fail-closed diagnostics, add a render path, keep the wrong lower→infer authority boundary. That is rational triage under review pressure, not laziness. It is still good-enough-for-now fixing with accounting, not structural payoff. Meta-verdict🔁 PAUSE_AND_REGROUP The direction is right, so revert is too strong. Real consumers were enabled, so this is not empty substrate growth. But the loop is now re-finding a known substrate bug class that the repo has already named structurally: post-lowering secondary authority / name recovery. Another round of local patching will add more tests and more surface area without settling the boundary. Stop iterating on instances. Write the next move as a structural rule and representation change: field projection must carry resolved child identity plus substitution context, and payload binding must become a boundary shape that cannot encode illegal states. Until that happens, the review loop is not paying debt down; it is relocating it. |
Director review — #458 (Prereqs 1+2)LGTM. Both prereqs implement the committed design answers from #455 correctly. Prereq 1 (§3.6 1a): Prereq 2 (§3.7 2e): Anti-patterns: none. No synthesized Declarations, no BranchPattern growth, no substrate.dag, no new semantic string lookups. Tests: 10 new + 1 emit unit test. Success, fail-closed (non-Conj, missing field, non-Disj, record variant rejection), generic SubstStack, and payload+field-access integration all covered. Design doc: Two follow-up items tracked (FieldProject phase carrier, generic call dispatch collapse). Correctly scoped. One minor gap: No test for empty path expression at the top of No blocking issues. |
|
ChatGPT review in progress... (view conversation) Check back in ~30 minutes for the full review. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
codex · gpt-5.4 · 773849bb
BLOCKING (1)
Root Cause
src/v3/compiler/src/infer.rsdecide_field_project computes field_decl_id as an ephemeral local and only writes the output TypeShape -> make FieldProject a phase carrier for resolved child identity and have infer fill it once so emit and upcoming reflection lenses consume the same fact.
Non-blocking — Strengths
src/v3/compiler/tests/m1_substrate_test.rsThe new tests cover both previously flagged inferred-scrutinee regressions, generic substitution, and fail-closed negative cases, which is the right consumer surface for substrate prerequisites.docs/substrate-reflection-design.mdThe design doc now records the post-458 follow-ups explicitly, which keeps the reflection loop honest instead of pretending the substrate is already done.
Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)
src/v3/compiler/src/infer.rsPayload-binding diagnostics fall back to the whole match span once BranchPattern resolves, so either carry the arm span on the resolved form or run payload binding before pattern rewrite; roadmap lane if deferred: prereq2 polish before reflection.
Loop health: 📈 CONVERGING — This round removes the two earlier lowering-time authority breaches and adds real consumer tests, so the loop is moving forward even though one narrower carry-forward issue remains.
| /// ResolvedIdentifier edges, looks up `field_label` on the | ||
| /// reached Conj, and resolves the output through the same | ||
| /// substitution context. No synthesized accessor declaration. | ||
| FieldProject { field_label: String }, |
There was a problem hiding this comment.
Invariant violation: BLOCKING: TransformTarget::FieldProject carries only field_label, so infer resolves the child declaration and then drops it, forcing downstream consumers to redo the projection walk instead of reading the resolved child fact structurally (Facts Flow Forward).
|
BLOCKING (1) Root Cause
Non-blocking — Strengths
Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)
Loop health: 📈 |
…tus + research framing Three updates to v3's self-hosting design note: - §2 L1 status: prereqs shipping (Prereqs 0-3 merged via #458/#460, Prereqs 4-5 in flight), reflection PR is next. Replaces stale "in design" label. - §2.1 (new): the pipeline is a .dag composition, not a file convention. Stages are typed functions composed via let bindings with explicit dependencies. Stage contracts are first-class (not decorative), per-stage fixed-point is structural, independent stages parallelize, and the compiler is analyzable by its own lenses. Pipeline declaration ships FIRST (model before implement); each stage starts as ExternalRealization during migration. - §5 (infer): explicitly framed as research, not engineering. I0 result cross-referenced (no decidability blocker). The open question narrows from "is this possible?" to "which write-surface option?" Also updates src/v3/ROADMAP.md M3 section to cross-reference SELF_HOSTING.md with key points. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…rence research framing (#464) * docs: update SELF_HOSTING.md with compositional pipeline + prereq status + research framing Three updates to v3's self-hosting design note: - §2 L1 status: prereqs shipping (Prereqs 0-3 merged via #458/#460, Prereqs 4-5 in flight), reflection PR is next. Replaces stale "in design" label. - §2.1 (new): the pipeline is a .dag composition, not a file convention. Stages are typed functions composed via let bindings with explicit dependencies. Stage contracts are first-class (not decorative), per-stage fixed-point is structural, independent stages parallelize, and the compiler is analyzable by its own lenses. Pipeline declaration ships FIRST (model before implement); each stage starts as ExternalRealization during migration. - §5 (infer): explicitly framed as research, not engineering. I0 result cross-referenced (no decidability blocker). The open question narrows from "is this possible?" to "which write-surface option?" Also updates src/v3/ROADMAP.md M3 section to cross-reference SELF_HOSTING.md with key points. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: §2.2 model every stage's domain to spec before implementation New section in SELF_HOSTING.md capturing the design principle: every pipeline stage models its inputs and outputs to spec BEFORE the stage body is implemented. Stage implementation is filling in function bodies over already-declared types — the same model- before-implement discipline the thesis demands of user programs, applied to the compiler itself. Per-stage domain modeling covers: parse (files, encodings, tokens, grammar as data), lower (surface AST as proper .dag Disj declarations with structural decompression), infer (rules as data operations, substitution stacks and scope as structural types), emit (full target language spec including rendering conventions). Between-stage contracts are the pipeline's function signatures — first-class, not decorative. A lens verifies each contract holds. The v2 lesson this prevents: types accreted reactively, downstream stages reconstructed facts instead of receiving them as typed edges. The annotate_descent_evidence pattern (33 heuristics in v2's complexity pass) is the canonical failure mode. Practical sequencing: model review → pipeline slot → implementation → parity test. Step 1 is where the hard thinking happens. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: add L2.5 per-stage domain modeling to dependency order Updates SELF_HOSTING.md §2 dependency diagram and gating rules: - L2.5 (per-stage domain modeling) runs in parallel with L2 (lens migrations). Both start after L1 (reflection). L2 writes lenses in dsl/lenses/; L2.5 declares pipeline-domain types in std/ and extdeps/. Independent work streams, no file overlap. - L2.5 stages proceed in L3's implementation order: emit domain first (partially exists), lower domain second, parse domain third, infer domain last (blocked on I3 write-surface experiment). Each domain model runs ahead of its stage's implementation. - New gating rule: L3 stage N cannot start until L2.5's model for stage N is reviewed. Implementation fills in function bodies over already-declared types. - Four-step sequencing table: model review → pipeline slot → implementation → parity test. - v3 ROADMAP.md M3 section updated with L2.5 in the dependency chain. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: address 3 review blockers on SELF_HOSTING.md §2.1/§2.2 Three fixes from codex review on #464: 1. §2.1 v2 contrast reframed. v2's compile.dag IS a .dag composition — the gap is decorative metadata with no consumers + no structural self-analysis + stage boundaries as convention not enforcement. Removed the claim that v2 "lacks a declared pipeline graph." 2. §2.1 typed boundary restated as lens-checked property. The infer output guarantee (all ports Resolved) is lens-enforced, not type-level — there is no InferredDag wrapper type. The doc now says "lens-checked property" explicitly and notes a future wrapper type as a stronger possible guarantee, not a current promise. 3. §2.2 substrate-vs-implementation split added. Walker-local state (SubstStack, Scope, UnificationState, fold locals) stays in stage .dag bodies, NOT in std/. Only cross-stage and downstream-consumed types go in std/. Rule: "if it crosses a boundary or a lens reads it, std/. If it's internal to one stage's walk, implementation." Table enumerates both categories. Infer domain bullet updated to match. Principle paragraph updated to say "at boundaries" not "universally." Also fixes stale Prereq 5 status (merged, not in flight). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: §2.3 language-agnostic compiler core + emission layering New section in SELF_HOSTING.md capturing three architectural commitments for omni-emission/ingestion: §2.3 — The compiler knows only substrate primitives (six connectives + five behaviors). It does NOT know what language it parses or emits. .dag is a GrammarSpec. Rust is a LanguageSpec. Both are data. The compiler is parametric on both input and output language. §2.3.1 — Emission/ingestion cost model. Any medium that can represent the substrate's primitives can be a target. Cost is structural: O(|substrate| × k^depth) where k is the expansion factor per nesting level. Well-matched targets (k ≈ 1) are cheap; poorly-matched targets (k > 1) grow exponentially with depth. Ingestion adds an information-deficit dimension — how much structural information the source language doesn't carry. §2.3.2 — Emission layering: spec vs preferences. Three layers with compositional opacity: Layer 1 (language specification — facts from the target's own spec), Layer 2 (representation mapping — substrate to target constructs), Layer 3 (style/lint/ idiom preferences — composable ON TOP of the spec). Quality of emitted code is a typed, composable property. The same layering applies to ingestion (grammar facts vs parsing preferences). §2.3.3 — Four design challenges: GrammarSpec formalism, LanguageSpec completeness, bootstrap seed size, per-language spec authoring cost. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: resolve single-authority blocker — pipeline supersedes bootstrap.dag Two fixes addressing the remaining review blockers on #464: 1. ROADMAP Track 17b + Phase 4: bootstrap.dag's stage vocabulary (CompilerStage, TransformContract, ChangeClassification, BootstrapStrategy) is explicitly superseded by the pipeline composition from SELF_HOSTING.md §2.1. regen.dag reads the pipeline's typed stage signatures, not a separate bootstrap.dag type set. Phase 4 Level 1-2 updated to reference pipeline signatures and lens-checked contracts instead of bootstrap.dag's TransformContract vocabulary. Resolves the "two authorities for stage metadata" finding both reviewers flagged. 2. SELF_HOSTING.md §2 gating rule 2: explicit distinction between L2.5 and the decorative-modeling pattern Track 17 warns about. Each L2.5 type has a named consumer: the L3 stage implementation that reads it. The test is: "which function body in L3 reads this type?" If you can't name one, don't declare it. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: fix §2.3 Shape A/B boundary + add ElaborationSpec + reframe StyleSpec Three fixes addressing ChatGPT review findings on #464: 1. Shape A / Shape B boundary respected. §2.3 now explicitly scopes to Shape A targets only. English, YAML, SPICE, and Terraform are never EmissionTarget values — they are Shape B outputs of .dag user programs. The thesis's category-error warning (§"Omni-emission") is referenced directly. The cost model in §2.3.1 keeps the expansion-factor analysis but separates Shape A cost (in LanguageSpec, compiler-owned) from Shape B cost (in user program type specs, user-owned). 2. GrammarSpec + ElaborationSpec split. The pipeline signature grows an elaboration parameter: grammar owns syntax (tokens → surface tree), elaboration owns semantics (surface → substrate). This matches MODELING.md's four-layer stack (surface sugar / composition / semantic kernel / foundation). Collapsing both into GrammarSpec would leave elaboration as implicit compiler behavior. New design challenge §2.3.3 #2 names the ElaborationSpec design question. 3. StyleSpec reframed as RenderingSpec — declared rendering conventions with structural authority. NOT "preferences" or "annotations." When present, they are hard constraints on the emitter's output formatting. "Optional" means the emitter CAN run without them, not that they are soft suggestions. Aligns with MODELING.md ("models are shared facts, not preferences") and INVARIANTS.md ("no annotation mechanisms through M3"). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: add Prereq 0.5 (implicit generic instantiation) + §4.4 (lens invocation) Two additions to substrate-reflection-design.md surfaced by the swift-ram-158 reflection implementer: Prereq 0.5 — Implicit generic-call instantiation. Prereq 0 lands explicit template binding (apply(3, negate)). Prereq 0.5 extends to implicit binding: when fold(singleton(1), 0, |acc, x| acc + x) is called, inference synthesizes T := Int, U := Int from argument types without explicit template arguments. This is the gap the *_int monomorphized wrappers in list.dag exist to bridge. Standard HM-style inference scoped to call sites, no new substrate variants. Blocks: lens migration (Unit 3), list.dag wrapper dissolution, compositional generic list operations. §4.4 — Lens invocation mechanism. Two paths: - Path A (compiled Rust integration) for parity tests — emitted Rust function linked into test binary, called with a Dag value, output compared byte-identical to Rust lens. Blocked on Prereq 0.5. - Path C (interpreter) for development and self-analysis — dag run evaluates the lens on a Dag value. No Rust compilation needed. Available earlier. - Path B (subprocess) rejected — awkward, slow, loses type safety. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: narrow RenderingSpec to visual-only + fix bootstrap.dag dissolution scope Two fixes from review feedback on #464: 1. RenderingSpec narrowed to strictly lexical/visual concerns. Removed Result<T,E> vs panic! (semantic — belongs in LanguageSpec), removed "idioms" field (semantic), removed ambiguity resolution from ingestion conventions (semantic — belongs in GrammarSpec or ElaborationSpec). Added explicit "MUST NOT change observable semantics" rule with test: if two RenderingSpec values produce programs with different runtime behavior, one contains a semantic choice that should be in LanguageSpec. 2. ROADMAP Track 17b authority note narrowed. Stage-contract vocabulary (CompilerStage, TransformContract, StageInput, StageOutput, FieldPropagation) is superseded by the pipeline. Schema-migration vocabulary (ChangeClassification, ChangeKind, BootstrapStrategy, FixedPointCheck) is NOT superseded — these remain as load-bearing types for SELF_HOSTING.md §10's patch pipeline until the schema-migration PR lands their first real consumer. Resolves the single-authority contradiction between §2.1 (pipeline supersedes) and §10 (schema-migration types are load-bearing). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…igration (#466) * docs: update SELF_HOSTING.md with compositional pipeline + prereq status + research framing Three updates to v3's self-hosting design note: - §2 L1 status: prereqs shipping (Prereqs 0-3 merged via #458/#460, Prereqs 4-5 in flight), reflection PR is next. Replaces stale "in design" label. - §2.1 (new): the pipeline is a .dag composition, not a file convention. Stages are typed functions composed via let bindings with explicit dependencies. Stage contracts are first-class (not decorative), per-stage fixed-point is structural, independent stages parallelize, and the compiler is analyzable by its own lenses. Pipeline declaration ships FIRST (model before implement); each stage starts as ExternalRealization during migration. - §5 (infer): explicitly framed as research, not engineering. I0 result cross-referenced (no decidability blocker). The open question narrows from "is this possible?" to "which write-surface option?" Also updates src/v3/ROADMAP.md M3 section to cross-reference SELF_HOSTING.md with key points. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: §2.2 model every stage's domain to spec before implementation New section in SELF_HOSTING.md capturing the design principle: every pipeline stage models its inputs and outputs to spec BEFORE the stage body is implemented. Stage implementation is filling in function bodies over already-declared types — the same model- before-implement discipline the thesis demands of user programs, applied to the compiler itself. Per-stage domain modeling covers: parse (files, encodings, tokens, grammar as data), lower (surface AST as proper .dag Disj declarations with structural decompression), infer (rules as data operations, substitution stacks and scope as structural types), emit (full target language spec including rendering conventions). Between-stage contracts are the pipeline's function signatures — first-class, not decorative. A lens verifies each contract holds. The v2 lesson this prevents: types accreted reactively, downstream stages reconstructed facts instead of receiving them as typed edges. The annotate_descent_evidence pattern (33 heuristics in v2's complexity pass) is the canonical failure mode. Practical sequencing: model review → pipeline slot → implementation → parity test. Step 1 is where the hard thinking happens. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: add L2.5 per-stage domain modeling to dependency order Updates SELF_HOSTING.md §2 dependency diagram and gating rules: - L2.5 (per-stage domain modeling) runs in parallel with L2 (lens migrations). Both start after L1 (reflection). L2 writes lenses in dsl/lenses/; L2.5 declares pipeline-domain types in std/ and extdeps/. Independent work streams, no file overlap. - L2.5 stages proceed in L3's implementation order: emit domain first (partially exists), lower domain second, parse domain third, infer domain last (blocked on I3 write-surface experiment). Each domain model runs ahead of its stage's implementation. - New gating rule: L3 stage N cannot start until L2.5's model for stage N is reviewed. Implementation fills in function bodies over already-declared types. - Four-step sequencing table: model review → pipeline slot → implementation → parity test. - v3 ROADMAP.md M3 section updated with L2.5 in the dependency chain. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: address 3 review blockers on SELF_HOSTING.md §2.1/§2.2 Three fixes from codex review on #464: 1. §2.1 v2 contrast reframed. v2's compile.dag IS a .dag composition — the gap is decorative metadata with no consumers + no structural self-analysis + stage boundaries as convention not enforcement. Removed the claim that v2 "lacks a declared pipeline graph." 2. §2.1 typed boundary restated as lens-checked property. The infer output guarantee (all ports Resolved) is lens-enforced, not type-level — there is no InferredDag wrapper type. The doc now says "lens-checked property" explicitly and notes a future wrapper type as a stronger possible guarantee, not a current promise. 3. §2.2 substrate-vs-implementation split added. Walker-local state (SubstStack, Scope, UnificationState, fold locals) stays in stage .dag bodies, NOT in std/. Only cross-stage and downstream-consumed types go in std/. Rule: "if it crosses a boundary or a lens reads it, std/. If it's internal to one stage's walk, implementation." Table enumerates both categories. Infer domain bullet updated to match. Principle paragraph updated to say "at boundaries" not "universally." Also fixes stale Prereq 5 status (merged, not in flight). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: §2.3 language-agnostic compiler core + emission layering New section in SELF_HOSTING.md capturing three architectural commitments for omni-emission/ingestion: §2.3 — The compiler knows only substrate primitives (six connectives + five behaviors). It does NOT know what language it parses or emits. .dag is a GrammarSpec. Rust is a LanguageSpec. Both are data. The compiler is parametric on both input and output language. §2.3.1 — Emission/ingestion cost model. Any medium that can represent the substrate's primitives can be a target. Cost is structural: O(|substrate| × k^depth) where k is the expansion factor per nesting level. Well-matched targets (k ≈ 1) are cheap; poorly-matched targets (k > 1) grow exponentially with depth. Ingestion adds an information-deficit dimension — how much structural information the source language doesn't carry. §2.3.2 — Emission layering: spec vs preferences. Three layers with compositional opacity: Layer 1 (language specification — facts from the target's own spec), Layer 2 (representation mapping — substrate to target constructs), Layer 3 (style/lint/ idiom preferences — composable ON TOP of the spec). Quality of emitted code is a typed, composable property. The same layering applies to ingestion (grammar facts vs parsing preferences). §2.3.3 — Four design challenges: GrammarSpec formalism, LanguageSpec completeness, bootstrap seed size, per-language spec authoring cost. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: resolve single-authority blocker — pipeline supersedes bootstrap.dag Two fixes addressing the remaining review blockers on #464: 1. ROADMAP Track 17b + Phase 4: bootstrap.dag's stage vocabulary (CompilerStage, TransformContract, ChangeClassification, BootstrapStrategy) is explicitly superseded by the pipeline composition from SELF_HOSTING.md §2.1. regen.dag reads the pipeline's typed stage signatures, not a separate bootstrap.dag type set. Phase 4 Level 1-2 updated to reference pipeline signatures and lens-checked contracts instead of bootstrap.dag's TransformContract vocabulary. Resolves the "two authorities for stage metadata" finding both reviewers flagged. 2. SELF_HOSTING.md §2 gating rule 2: explicit distinction between L2.5 and the decorative-modeling pattern Track 17 warns about. Each L2.5 type has a named consumer: the L3 stage implementation that reads it. The test is: "which function body in L3 reads this type?" If you can't name one, don't declare it. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: fix §2.3 Shape A/B boundary + add ElaborationSpec + reframe StyleSpec Three fixes addressing ChatGPT review findings on #464: 1. Shape A / Shape B boundary respected. §2.3 now explicitly scopes to Shape A targets only. English, YAML, SPICE, and Terraform are never EmissionTarget values — they are Shape B outputs of .dag user programs. The thesis's category-error warning (§"Omni-emission") is referenced directly. The cost model in §2.3.1 keeps the expansion-factor analysis but separates Shape A cost (in LanguageSpec, compiler-owned) from Shape B cost (in user program type specs, user-owned). 2. GrammarSpec + ElaborationSpec split. The pipeline signature grows an elaboration parameter: grammar owns syntax (tokens → surface tree), elaboration owns semantics (surface → substrate). This matches MODELING.md's four-layer stack (surface sugar / composition / semantic kernel / foundation). Collapsing both into GrammarSpec would leave elaboration as implicit compiler behavior. New design challenge §2.3.3 #2 names the ElaborationSpec design question. 3. StyleSpec reframed as RenderingSpec — declared rendering conventions with structural authority. NOT "preferences" or "annotations." When present, they are hard constraints on the emitter's output formatting. "Optional" means the emitter CAN run without them, not that they are soft suggestions. Aligns with MODELING.md ("models are shared facts, not preferences") and INVARIANTS.md ("no annotation mechanisms through M3"). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * docs: add Prereq 0.5 (implicit generic instantiation) + §4.4 (lens invocation) Two additions to substrate-reflection-design.md surfaced by the swift-ram-158 reflection implementer: Prereq 0.5 — Implicit generic-call instantiation. Prereq 0 lands explicit template binding (apply(3, negate)). Prereq 0.5 extends to implicit binding: when fold(singleton(1), 0, |acc, x| acc + x) is called, inference synthesizes T := Int, U := Int from argument types without explicit template arguments. This is the gap the *_int monomorphized wrappers in list.dag exist to bridge. Standard HM-style inference scoped to call sites, no new substrate variants. Blocks: lens migration (Unit 3), list.dag wrapper dissolution, compositional generic list operations. §4.4 — Lens invocation mechanism. Two paths: - Path A (compiled Rust integration) for parity tests — emitted Rust function linked into test binary, called with a Dag value, output compared byte-identical to Rust lens. Blocked on Prereq 0.5. - Path C (interpreter) for development and self-analysis — dag run evaluates the lens on a Dag value. No Rust compilation needed. Available earlier. - Path B (subprocess) rejected — awkward, slow, loses type safety. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com> * Advance reflected substrate and runtime emission * Advance reflected runtime carrier and address review feedback * Extend payload binding and structural recursion checks * Make v3 List structural during bootstrap * Canonicalize specialized generic signature shapes * Advance reflected lens execution path * Migrate unused-parameters lens to emitted shim * Add freshness gate for emitted lens snapshot * Tighten reflected realization validation * Drop dead syntax binding fields * Fix v3 clippy regressions * Fix remaining v3 clippy targets * Finish remaining lens migration review fixes --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 participant
Summary
Implements the two locked compiler-side prerequisites from the substrate reflection design work:
Prereq 1: field-access lowering
TransformTarget::FieldProject { parent_type, field_label }value.fieldinto one projectionTransformper segmentemit_rustto handle the new target directlyPrereq 2: match-with-payload-binding
SurfacePattern::VariantWith { name, binding, span }PayloadBindingplusPath.binding: Option<PayloadBinding>BranchPatternat its existing two variantsThe branch is intentionally split into two commits, one per prereq, because both changes touch
lower.rsand the shared PR avoids merge churn there.Why
PR #455 locked the design answers for these two prerequisites after PR #453 showed the failure modes:
BranchPatterngrowth for payload bindingThis implementation follows those decisions directly:
FieldProjecttransform targetPath.binding, separate fromBranchPatterndiscriminationNon-goals
src/v3/std/substrate.dagDeclarationRefrename from PR v3: rename v3_l1.Declaration sentinel to DeclarationRef #456BranchPatternbeyond its current two variantsValidation
cargo test -p v3-compilercargo clippy -p v3-compiler --all-targets -- -D warningsCommit split
v3: lower local field access to FieldProjectv3: add match payload binding on Path