[codex] Land Prereq 0, Prereq 3, and I0 by briansrls · Pull Request #460 · gunb-ai/gunbc

briansrls · 2026-04-15T23:42:43Z

Summary

This PR lands the clean main-based version of the Prereq 0, Prereq 3, and I0 work.

It includes:

Prereq 0 as the locked §3.5 option 1c implementation.
Higher-order function arguments bind through Instantiation / TemplateArgument plus SubstStack propagation rather than through a new substrate call target or monomorphized specializations.
Prereq 3 as the first honest lambda landing.
The parser accepts |...| expr, lowering turns lambdas into ordinary Bind-backed callable declarations with captures materialized as additional positional inputs, and call sites pass only the declared runtime parameters.
I0 result capture.
The decidability paper exercise is written up in-tree and records a pass for the literal-filling rule plus a bounded structural walk spot-check.

Why

#458 already merged the Prereq 1 / Prereq 2 work onto main. The earlier #457 stack had base-branch contamination from the old #453 line of work, so this PR republishes the intended Prereq 0 / Prereq 3 / I0 scope cleanly on top of current main.

This keeps the branch aligned with the committed design answers:

Prereq 0 stays on Instantiation + SubstStack
Prereq 3 stays on ordinary Bind with captures as explicit inputs
I0 stays documentation-only and reports a bounded decidability pass

Scope notes

The lambda landing is intentionally contextual in this first pass:

lambdas lower when an expected function type is already available, such as a function-typed argument position or an annotated let
unannotated standalone lambda values fail closed instead of guessing a function type
the callback-rule lens test remains follow-up work and is still tracked as such in the design docs

User / developer impact

Developers can now:

pass named functions through higher-order signatures under the locked 1c design
write contextual lambdas like let f: fn(Int) -> Int = |x| x and apply_to_three(|x| base + x)
rely on regression coverage for nested higher-order substitution, outer-callable capture, and fail-closed conflicting callable template bindings

Validation

Ran locally:

cargo test -p v3-compiler
cargo clippy -p v3-compiler --all-targets -- -D warnings

briansrls · 2026-04-15T23:44:58Z

ChatGPT review in progress... (view conversation)

Check back in ~30 minutes for the full review.

briansrls · 2026-04-15T23:49:21Z

Director review — #460 (Prereqs 0+3+I0, clean main rebase)

LGTM. Clean rewrite of #457's HEAD commit onto main. No contamination from the old #453 branch.

Contamination check: clear. No substrate.dag, no BranchPattern growth, no FieldAccessor synthesis, no build.rs/v3_l1.dag/rust.dag changes. The sole VariantWith reference is a read of the existing SurfacePattern::VariantWith inside collect_lambda_free_names — correct usage, not a new addition.

Prereq 0 (1c): confirmed. TemplateArgument doc updated, SubstStack wired in resolve_arrow_walk, bind_expected_type_to_actual unifies Arrow shapes with depth bound. No new substrate variants.

Prereq 3 (contextual lambda): confirmed. Parser, lowering to Bind with captures as extra params, call-site rewrite (callable args continue past runtime port push). Contextual limitation documented in two places. Unannotated lambdas fail closed with diagnostic.

#458 compatibility: clean. Uses local_scope_from_parent from Prereq 1 correctly. No conflicts with FieldProject or PayloadBinding.

Tests: 9 new. Single/nested HoF, annotated/multi-param/captured lambda, lambda-as-HoF-arg, outer-callable capture, conflicting-callable fail-closed, unannotated-lambda fail-closed. Both success and failure paths covered.

I0: adequate. Same content as #457, correctly scoped as first pass.

One non-blocking item carried forward: declaration_is_callable still duplicated between infer.rs (standalone recursive) and lower.rs (delegates to declaration_callable_inputs). Semantically identical. Recommend extracting to shared utility in a follow-up.

No blocking issues. Ship-ready.

chatgpt-codex-connector

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b5f8235105

ℹ️ 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".

chatgpt-codex-connector · 2026-04-15T23:55:55Z

+            if let Some(lambda_decl_id) = lambda_callable {
+                scope.callables.insert(name.clone(), lambda_decl_id);


Clear stale callable binding on let rebinding

This updates scope.values for every let but only mutates scope.callables when the new expression is a lambda, so an older callable entry survives when a name is rebound to a non-callable value. In a sequence like let f: fn(Int)->Int = |x| x; let f: Int = 0; let y = f(1), call resolution will still target the old lambda instead of rejecting f as non-callable, which violates lexical shadowing and can silently execute the wrong function.

Useful? React with 👍 / 👎.

chatgpt-codex-connector · 2026-04-15T23:55:55Z

    let mut param_ports: Vec<PortId> = Vec::with_capacity(params.len());
    let mut param_types: Vec<TypeShape> = Vec::with_capacity(params.len());
    let mut body_scope: HashMap<String, PortId> = outer_scope.clone();
+    let mut callable_scope: CallableScope = CallableScope::new();


Preserve outer callable scope when lowering fn bodies

Function-body lowering starts with an empty callable_scope, so callable bindings created by earlier let items are dropped even though their value ports are in outer_scope. That makes valid lexical references fail, e.g. let inc: fn(Int)->Int = |x| x + 1 followed by fn use(n: Int) -> Int = inc(n) cannot resolve inc as a call target inside use because only parameter callables are tracked.

Useful? React with 👍 / 👎.

…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>

v3: land Prereq 0, Prereq 3, and I0

b5f8235

briansrls marked this pull request as ready for review April 15, 2026 23:49

docs: cross-reference I0 fixpoint analysis

92a7e53

briansrls merged commit 5085849 into main Apr 15, 2026
2 checks passed

chatgpt-codex-connector Bot reviewed Apr 15, 2026

View reviewed changes

briansrls mentioned this pull request Apr 16, 2026

[codex] v3: bootstrap staged std.list and list roundtrips #463

Merged

briansrls mentioned this pull request Apr 16, 2026

docs: SELF_HOSTING.md — compositional pipeline + prereq status + inference research framing #464

Merged

2 tasks done

briansrls mentioned this pull request Apr 17, 2026

Reflective analysis — 3-day integration review #392

Closed

briansrls deleted the prereq0-prereq3-i0-rewrite branch June 1, 2026 18:41

Navigation Menu

Repository navigation

[codex] Land Prereq 0, Prereq 3, and I0 - #460

[codex] Land Prereq 0, Prereq 3, and I0#460
briansrls merged 2 commits into
mainfrom
prereq0-prereq3-i0-rewrite

briansrls commented Apr 15, 2026

Uh oh!

briansrls commented Apr 15, 2026

Uh oh!

briansrls commented Apr 15, 2026

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

chatgpt-codex-connector Bot Apr 15, 2026

Uh oh!

chatgpt-codex-connector Bot Apr 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

		if let Some(lambda_decl_id) = lambda_callable {
		scope.callables.insert(name.clone(), lambda_decl_id);

Conversation

briansrls commented Apr 15, 2026

Summary

Why

Scope notes

User / developer impact

Validation

Uh oh!

briansrls commented Apr 15, 2026

Uh oh!

briansrls commented Apr 15, 2026

Director review — #460 (Prereqs 0+3+I0, clean main rebase)

Uh oh!

Uh oh!

chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

chatgpt-codex-connector Bot Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

chatgpt-codex-connector Bot Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant