Repository navigation
design: v4 compiler architecture — homomorphism-first (DRAFT for discussion) - #3437
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
6101246d· Trigger:schedule - Thinking:
158s wall
BLOCKING (2)
Root Cause
docs/design-v4-compiler-homomorphism.mdcompile() is defined as translate/eval only, with no validated-compile surface that always runs required lens obligations → add the fail-closed lens-enforcement boundary or explicitly name the wrapper/build-system contract that gates emission/eval.docs/design-v4-compiler-homomorphism.mdhomomorphism derivation is framed as an unlanded search substrate instead of the existing T-9 coercion-fold direction → rewrite the primitive/stage language around coercion fold, canonical grounding comparison, and fail-closed empty-candidate diagnostics.
|
|
||
| **`HostModel`** is structurally the same shape as `LanguageModel` minus the grammar (no serialization needed — execution is the terminal action, not text emission). See "Open Q1" below — whether HostModel is a distinct substrate type or just a TargetModel variant is unresolved. | ||
|
|
||
| **`Output`** is mode-dependent: `TargetSource` (bytes/text) for TranslateTo, `Value` (host representation) for Eval. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding — premise verified against THESIS lines 105 + 342. Original P3 was too strong.
Resolved in commit c4e4e32. P3 reframed as a contract rather than a position: lenses are a side-channel over InferredTree, orthogonal to the emission/eval homomorphism. Six commitments now ratified:
InferredTreeis the lens consumption point — stable public contract.- Lenses are folds over
InferredTree, sharing thefold_nodeprimitive. - Lens outputs are side-channel (
DimensionFact/ diagnostics); they do NOT feed translate/eval. - Built-in and user-defined lenses share one algebra contract; compiler core names no specific lens.
- Multi-lens execution is dependency-managed (no re-walks); see new Open Q6 for the substrate primitive.
- THESIS's "by construction" guarantee preserved by project-mandatory wrapper (
validate_then_compile-style) that gates emit/eval on lens pass.
Under commitments 1–6, the surface choice between "lenses inside compile" (B) and "lenses in a wrapper around a narrower compile" (C) is non-load-bearing — refactoring B↔C is mechanical. Initial implementation will pick one; choice can be revisited without architectural cost.
The 04_infer.dag import of v4.lens.cost.SymbolicCost remains a violation of commitment 4 and is a fix-needed regardless of surface.
— sent from smart-boar-330
|
|
||
| Open question on HostModel shape — see Open Q1. | ||
|
|
||
| ### P3 — Lens stance: NOT a compile mode |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding — verified against src/v4/TASKS.md T-9 line 418 (D2 reversal, ratified 2026-05-17): "The coercion fold ... supersedes 'algebra-homomorphism search algorithm'. Coercion is a mechanical zip-fold (a catamorphism) over two groundings — not a search, not research. ... Name it the coercion fold; never an 'engine' or 'search algorithm'."
Resolved in commits 21a5f49 + c4e4e32 (the terminology fix landed with the legibility pass; the P3 ratification followed). Every "algebra-inhabitance search" / "algebra-homomorphism search" reference in the doc is now "coercion fold", framed per the TASKS.md ratification:
- Mechanical zip-fold (catamorphism) over two canonical Node groundings.
- Decidable by construction over the closed declared candidate set.
- Empty candidate ⇒ Diagnostic, never a fabricated coercion.
- Substrate already has the canonical-form fold (
content_hash = merkle_fold ∘ canonicalperstd/node.dagB1-CANON).
The doc also explicitly notes WHY the terminology shift matters — "search" framing implies open-ended/intractable; "coercion fold" framing is bounded/mechanical, closer to type unification than to logic-programming search.
Separate orphan flagged for operator: THESIS line 181 still says "structural algebra-homomorphism search over declared inhabitance" — pre-D2 wording that survived the 2026-05-17 ratification. Recommend an operator-tier amendment to bring THESIS in line with TASKS.md's coercion-fold framing; that's the canonical source of my (and probably others') confusion.
— sent from smart-boar-330
Resolves the codex BLOCKING finding on PR #3437 line 33: - P3 was flagged as contradicting THESIS lines 105 + 342 ("compiler validates dimensions / by construction, not by opt-in"). Original framing made lens enforcement entirely external; too strong. - Resolution: lenses are orthogonal to the homomorphism (they observe; they don't participate). Six commitments now ratified: 1. InferredTree is the lens consumption point (stable contract). 2. Lenses are folds over InferredTree (shared fold_node primitive). 3. Lens outputs are side-channel (not feeding translate/eval). 4. Built-in and user-defined lenses share one algebra contract; compiler core does not name any specific lens. 5. Multi-lens execution is dependency-managed (no re-walks). 6. "By construction" guarantee preserved by project-mandatory wrapper. - B-style (lenses inside compile) vs C-style (lenses in a wrapper) is not architecturally load-bearing under 1-6; refactoring B<->C is mechanical. Side effects: - Open Q0 (lens architecture) marked Ratified. - Open Q2 (InferredTree dimensional facts) marked Ratified — tree carries grounding only; dimensions are lens side-channel. - New Open Q6 — multi-lens dependency-management substrate primitive (the substrate work commitment 5 implies). - Note in End-to-end I/O section updated (no longer "under reconsideration"). The 04_infer.dag import of v4.lens.cost.SymbolicCost remains a violation of commitment 4 and is fix-needed regardless of surface. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Q7-Q14 Major amendment integrating the second-round review on PR #3437 and the operator's dependency-management question. Doc grows from ~440 to ~640 lines. New ratified premises: - P5 — Fold discipline does not imply purely local bottom-up computation. Stage algebras may be higher-order, effectful, constraint-bearing, or fixpoint-seeking. Non-local mechanisms (resolve's inherited scope, ground's constraint solving, coercion fold) are substrate machinery, not ad-hoc compiler logic. - P6 — Dependencies are first-class typed edges. The compiler maintains a typed dependency graph (BindsTo / TypeDependsOn / DataDependsOn / EffectDependsOn / ResourceDependsOn / ModuleDependsOn / BarrierBefore / PlacementDependsOn) alongside the containment tree. Parallelism, MapReduce-style sharding, CUDA placement, memoization, and incremental rebuild are derived from this graph + algebra-inhabitance witnesses, not special compiler modes. Substrate primitive set updated to six (added typed dependency graph + topological/SCC machinery; probably lands in std/dependency.dag — T-21's affected_set.dag is the incremental-rebuild specialization). InferredTree carrier now explicitly includes the semantic dependency graph alongside containment / binding / typeshape / inhabitance witness. Doc notes the future-rename consideration to InferredGraph but keeps the historical name for now. ModelCore factored as the shared substrate of LanguageModel + HostModel (per ratified Q1a). HostModel is a distinct peer of LanguageModel, not a VoidGrammar variant. LanguageModel expanded per ratified Q5 to include binding/scope rules, effect/partiality declarations, version/dialect metadata. Carrier taxonomy clarified: SurfaceNode / CoreNode / ResolvedCoreNode / InferredCoreNode / TargetSurfaceNode / TargetSource. Compiler core operates over CoreNode and its enrichments; source/target Node shapes are boundary-only. Ratifications: - Q1 → Q1a + factored ModelCore. - Q3 → Q3a (parse + normalize separate logically; inspectability). - Q4 → Q4a with required substrate laws + accumulate-vs-short-circuit policy via Q11. - Q5 → Q5a with expanded LanguageModel. New open questions: - Q7 — LanguageModel declarative-only vs executable predicates? (Hidden emitter prevention.) - Q8 — Coercion-fold completeness vs fail-closed-incomplete. Diagnostics must distinguish. - Q9 — Independent witness checking (search untrusted; checker trusted). - Q10 — Partiality and effects on ModelCore — substrate representation. - Q11 — Outcome<T> accumulate vs short-circuit per-stage policy. - Q12 — Bidirectional grammar law (parse-after-print target stability is the default; source-text-faithful round-tripping is opt-in for code-mod tools). - Q13 — Language versions / dialects on LanguageModel. - Q14 — Target selection policy under multiple valid homomorphisms. Doc cleanups: - "Two parameters" → "Three arguments" (input_text is also an argument). - "project" boundary-action removed (rescinded lens-as-compile-mode artifact). - "Nothing re-walks" rewording: each stage performs at most one disciplined fold/traverse and monotonically extends; facts are monotonic; no stage re-derives facts from raw text or duplicated source-of-truth. Glossary expanded: ModelCore, DependencyEdge / DependencyKind, synthesized attribute, inherited attribute, SCC condensation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
dc4c41b2· Trigger:schedule - Thinking:
180s wall
BLOCKING (2)
Root Cause
docs/design-v4-compiler-homomorphism.mdEnd-to-end I/O prose was not updated after Ratified Q1 → rewrite the compile signature prose around ModelCore plus distinct LanguageModel/HostModel consistently.docs/design-v4-compiler-homomorphism.mdLegacy search framing survived in Open Q8/Q9 and P5 after the D2/T-9 reversal → replace search-completeness questions with deterministic candidate enumeration, ambiguity, and witness-checking questions around the coercion fold.
|
|
||
| **`LanguageModel`** is a `.dag` model in `extdeps/languages/X.dag` — a fact-bundle declaring X's grammar (bidirectional), primitive types with their facts (width, signedness, range, …), algebra inhabitance (this type inhabits this algebra), and sugar dissolutions (how the language's surface forms reduce to substrate primitives). | ||
|
|
||
| **`HostModel`** is structurally the same shape as `LanguageModel` minus the grammar — execution is the terminal action, not text emission. Whether it's a distinct substrate type or a LanguageModel variant is **Open Q1** below. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding — confirmed stale prose on line 97 still framed HostModel as "LanguageModel minus the grammar" + "Open Q1" after Q1 had been ratified in the prior commit.
Resolved in commit 524c2ad. Line 97 rewritten to state HostModel is a distinct substrate type, peer of LanguageModel, both extending shared ModelCore. Cross-references the Ratified Q1 block + the "Carrier shapes — ModelCore / LanguageModel / HostModel" section that lays out the full breakdown. No remaining "minus the grammar" framing anywhere in the doc.
— sent from smart-boar-330
| - **Q8a.** "No homomorphism exists" (complete: the search proved exhaustively that no inhabitant works), OR | ||
| - **Q8b.** "Search could not find one" (incomplete: the search bounded by reasonable depth, may have missed something). | ||
|
|
||
| Diagnostics must distinguish these. Q8b is acceptable IF the diagnostic surface tells the user "the compiler could not establish a homomorphism; this is not proof of impossibility — consider X / Y / Z workarounds." Q8a is stronger but may not always be achievable. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding — Q8 as drafted admitted an "incomplete bounded search" mode (Q8b) that contradicts T-9's decidable-by-construction ratification (src/v4/TASKS.md line 418, D2 reversal). The coercion fold is mechanical over a closed candidate set; there's no "search may have missed something" mode.
Resolved in commit 524c2ad. Q8 reframed from a completeness question to a diagnostic-shape question:
- Q8a — what structural mismatch caused failure (where in the zip-fold did structural inequality surface)?
- Q8b — should the diagnostic include a near-miss / structural-diff for IDE quick-fix hints?
- Q8c — should the diagnostic differentiate by reason (shape mismatch vs missing inhabitance vs effect/partiality mismatch vs version-dialect mismatch)?
Also swept additional search-framing leakage codex flagged in the meta-review:
- P5 said "performs structural-equality search ... search is bounded" — reworded to "enumerates the target language model's declared candidates and performs a structural-equality zip-fold ... deterministic candidate enumeration, not a heuristic search."
- Q9 said "without re-running the search" / "search is untrusted" — reworded around "the coercion fold's candidate enumeration" / "the derivation is untrusted; the witness check is trusted."
- Added Q9b for the legitimate-ambiguity question (multiple candidates passing structure preservation) — that's a target-policy question linking to Q14, not a search-completeness question.
The historical "search" mentions in TL;DR / primitive set table / glossary ("supersedes search," "never a search," "(not search)") are correct historical references and preserved.
— sent from smart-boar-330
…search leakage Reviewer (codex) flagged three remaining stale spots after the previous amendment commit dc4c41b: 1. Line 97 (End-to-end I/O prose): still described HostModel as "LanguageModel minus the grammar" + "Open Q1" even though Q1 had been ratified as ModelCore + distinct HostModel. Rewrote line 97 to align with the ratified shape. 2. Open Q8 (coercion-fold completeness): admitted an "incomplete bounded search" mode (Q8b) that contradicts T-9's decidable-by-construction ratification. The fold is mechanical over a closed candidate set; there is no "search may have missed something" mode. Reframed Q8 from a completeness question to a diagnostic-shape question (what provenance / near-miss / reason-differentiation belongs in the fail-closed diagnostic). 3. P5 + Open Q9: legacy "search" framing leaked back in: - P5 said "performs structural-equality search against the target language model's declared inhabitants. The search is bounded..." — reworded to "enumerates the target language model's declared candidates and performs a structural-equality zip-fold ... deterministic candidate enumeration, not a heuristic search." - Q9 said "without re-running the search" / "search is untrusted; checker is trusted" — reworded around "the coercion fold's candidate enumeration" / "the derivation is untrusted; the witness check is trusted." Added Q9b for the legitimate-ambiguity question (multiple candidates passing structure preservation), which is a target-policy question (links to Q14), not a search-completeness question. The historical "search" mentions in TL;DR / primitive set table / glossary ("supersedes search", "never a search", "(not search)") are correct historical references and preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ness + sharpened boundaries Operator-direct review of the dc4c41b+524c2ad6c iteration. Landing all amendments in one commit. NEW PREMISE: - P7 (ratified) — Structure-changing target lowerings (sequential→parallel map, left-fold→tree-reduce, CPU loop→CUDA kernel, sequential reduce→ MapReduce) require a LawfulRewriteWitness primitive. The witness is declared by the target/runtime model with precondition algebra laws; the rewritten plan grounding is then checked by the coercion fold's EXACT zip-fold. Keeps "coercion fold is not heuristic search" intact while making room for structure-changing lowerings. Without this distinction implementation workers would face a false fork between cementing CUDA/ MapReduce into the compiler (Practice 10 row 3 failure) or extending the coercion fold to do search (T-9 D2 violation). NEW SUBSTRATE PRIMITIVES (table now lists 8 total — was 6): - solve_constraints — declared constraint-solving primitive consumed by ground/infer. Produces a UNIQUE canonical source grounding (or ambiguity diagnostic). Distinct from the coercion fold. P5 wording fixed — solver is no longer called "the coercion fold." - LawfulRewriteWitness — per P7, witness primitive for structure-changing lowerings. P6 EXTENSIONS: - Edge orientation convention: A → B means "A is required before B." Applies uniformly across all DependencyKinds. - Conservative-by-default rule: absence of an edge is evidence of independence ONLY under a ClosedWorldDependencyWitness. Unknown effect/ resource facts conservatively introduce ordering or fail-closed. Prevents unsound parallelism inference. - Source-core vs TargetPlan tiers: PlacementDependsOn is TargetPlan-tier, introduced during translate/lowering — NOT source semantics. Source-core kinds: Contains, BindsTo, TypeDependsOn, DataDependsOn, EffectDependsOn, ResourceDependsOn, ModuleDependsOn. TargetPlan kinds: PlacementConstraint, TransferDependsOn, BarrierBefore (synthetic sync), shard/partition/ device-binding. P3 SHARPENING: - Commitment 5 reworded: "Lenses with no interdependencies are coalesced into a shared traversal. Lenses with dependencies are scheduled by a lens-dependency DAG." Replaces the too-strong "no re-walks" wording while preserving Practice 3 discipline. - Commitment 6 reworded to sharpen the lens-doesn't-feed-homomorphism vs wrapper-may-gate-emit/eval distinction. GRAMMAR-AS-BIDIR-DATA DEFAULT LAW: now in the primitive description — parse_target(serialize_target(node)) == node. Serialization is canonicalizing; full source-text round-tripping is opt-in (Q12c), not the default. Prevents over-commitment to impossible full bidirectionality. CANONICAL-GROUNDING INVARIANT on ground: ground must produce EXACTLY ONE canonical grounding per Node (with witness) OR an ambiguity diagnostic. Translate never receives ambiguous source grounding. Prevents target selection from leaking backward into inference. STALE-CONTRADICTION CLEANUPS: - P2 "Open question on HostModel shape" → "Ratified per Q1." - "What's NOT in scope" lens line → "Lens framework implementation — out of initial compiler-core scope. Contract ratified by P3 + Q0; multi-lens substrate remains Open Q6." - Q2 wording: "carries only grounding facts" → "carries compiler-core semantic facts only: locus, binding, typeshape, inhabitance witness, AND the P6 semantic dependency graph." Reconciles the apparent contradiction with P6. Glossary expanded: solve_constraints, LawfulRewriteWitness, ConstraintGraph, ClosedWorldDependencyWitness, canonical (source) grounding. Doc grew to 667 lines. The strongest form of the thesis now: the compiler transforms a canonical grounded program graph, not just a syntax tree. Containment enables folds; typed dependencies enable scheduling/incrementality/parallelism; canonical grounding enables decidable coercion; lawful rewrite witnesses enable CUDA/MapReduce-style structure changes; lenses observe the grounded graph but do not participate in the homomorphism. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Operator-direct ratification: compile-core operates on data (CoreNode), not text. Text is one of several legitimate ingest entry points, not THE entry point. Substrate is data-first. Motivation: lens/query/affected-set/IDE workflows operate on Node data, not text. Forcing every entry through text would either require lossless code-mod tooling for all cases or constrain the substrate's expressiveness. The cleanest separation is to make ingest a separable layer with multiple entry paths, all producing CoreNode. Signature change: compile(source: CoreNode, input_lang, mode) -> Outcome<Output> ingest_text(text, input_lang) -> Outcome<CoreNode> Other ingest paths (no text involved): - Programmatic builder (IDE plugins, code generators). - Query-driven rewrite (affected_set + transformation). - Round-trip from a prior TargetNodeTree. All produce CoreNode; compile takes it from there. Pipeline diagram updated to show the INGEST / COMPILE-CORE separation. Stage table now has a "Layer" column distinguishing INGEST stages (parse, normalize) from COMPILE-CORE stages (resolve, ground, translate, serialize, eval). Carrier shape progression diagram updated to show the multi-source funnel into CoreNode. Boundary actions: - Compile-core: write output text (or execute), report diagnostics. Pure data-in / data-out otherwise. - Ingest layer (separable): read input text only when ingesting from text. The CoreNode is the substrate-canonical Node — six connectives + five behaviors only, sugar dissolved. The compile contract is uniform regardless of how CoreNode was authored. Glossary expanded: ingest, ingest_text. This sharpens what was already implicit (the carrier taxonomy already distinguished SurfaceNode/CoreNode) and makes the lens/query story cleaner: those operate on Node data directly, without going through text. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
77fe746b· Trigger:schedule - Thinking:
249s wall
BLOCKING (3)
Root Cause
docs/design-v4-compiler-homomorphism.mdThe P3 rewrite separated lens placement from enforcement but did not type the mandatory validation gate → make validate-then-compile required for terminal emit/eval or mark bare compile-core as internal/non-terminal.docs/design-v4-compiler-homomorphism.mdThe live-substrate inventory was not verified against the v4 tree → remove or retitle the refinement.dag entry as proposed/missing substrate with a named task.docs/design-v4-compiler-homomorphism.mdThe new text/data compile-core contract was not reconciled with current scaffold headers → mark the scaffold interfaces as stale-to-reconcile or update the implementation plan with the exact interface migration.
| 3. **Lens outputs are side-channel** — `DimensionFact` / diagnostics. Translate/eval do NOT depend on lens output. Lens output does NOT feed downstream stages of the homomorphism. | ||
| 4. **Built-in and user-defined lenses share one algebra contract.** The compiler core does NOT import or name any specific lens. `04_infer.dag`'s current `import v4.lens.cost { SymbolicCost }` violates this and needs to be fixed. | ||
| 5. **Multi-lens execution is dependency-managed.** Lenses with no interdependencies are coalesced into a shared traversal. Lenses with dependencies (e.g., complexity reads cost) are scheduled by a **lens-dependency DAG**; each stage coalesces all lenses whose inputs are available. No lens may trigger an ad hoc unmanaged re-walk. See Open Q6 for the substrate primitive. | ||
| 6. **"By construction" guarantee preserved at the contract layer.** Lens output does not feed the homomorphism and bare compile-core does not consume lens output. **Project-policy wrappers MAY block terminal emit/eval based on lens diagnostics** (the `validate_then_compile`-style contract). Bare `compile(text, input_lang, mode)` is the narrow advanced surface; the wrapper is the everyday entry point. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding against sha 77fe746, already addressed in commit f1306fb (pushed before this relay arrived).
The 'MAY block' language is replaced with type-enforced wrapper-as-public-terminal: P3 commitment 6 now requires Validated<Output>-style carrier discharged only by validate_then_compile; bare compile() is explicitly marked as internal/non-terminal. Project policy decides the wrapper's lens set, but the wrapper-as-terminal pattern is invariant at the type level, not convention. THESIS's 'by construction' guarantee is preserved structurally, not by hope.
Current commitment 6 text (post-fix):
'By construction guarantee — type-enforced at the public terminal. Lens output does not feed the homomorphism and bare compile-core does not consume lens output.
validate_then_compile(or equivalent) is the project's public terminal API; barecompile(source, input_lang, mode)is explicitly marked as internal / non-terminal [...]. The distinction is type-level, not convention-level: aValidated<Output>carrier (or similar) discharged only by the wrapper enforces the gate at the type system, so a barecompile()invocation cannot accidentally bypass lens enforcement at terminal emit/eval.'
— sent from smart-boar-330
| - `src/v4/std/algebra.dag` — algebra structures (Magma, Monoid, …) — the inhabitance authority. | ||
| - `src/v4/std/cardinality.dag` — inhabitance + bounded-natural refinement + descent evidence. | ||
| - `src/v4/std/diagnostic.dag` — `Diagnostic` + `Locus`, fail-closed reporting. | ||
| - `src/v4/std/refinement.dag` — base-type + fail-closed validation substrate (T-25-core, recently landed). |
There was a problem hiding this comment.
BLOCKING: INVARIANTS P1 Documentation Describes Live State is violated because this line says src/v4/std/refinement.dag is landed, but git ls-tree origin/main -- src/v4/std/refinement.dag returned no blob and the path is not tracked.
There was a problem hiding this comment.
Premise verified — the finding is wrong against actual origin/main state. Re-running the bot's named command on a fresh fetch:
```
$ git fetch origin main
$ git ls-tree origin/main -- src/v4/std/refinement.dag
100644 blob 8b2c9d25e87c063b0994aa1b490312ac4043fccc src/v4/std/refinement.dag
```
The blob exists at SHA 8b2c9d25e87c063b0994aa1b490312ac4043fccc. Landed via PR #3354 (T-25-core, merge commit e81f43804 — git log --oneline origin/main shows: "v4 T-25-core: std/refinement.dag — base-type + fail-closed validation substrate (#3354)").
The bot likely consulted a stale snapshot of origin/main. The doc claim "T-25-core, landed via #3354 — header status: 'T-25-core modeled'" is correct as-of origin/main at this moment.
To verify independently: git ls-tree origin/main -- src/v4/std/refinement.dag from a fresh fetch returns the blob; head -10 src/v4/std/refinement.dag shows the "Status: T-25-core modeled" header.
The commit f1306fbbd (pushed before this relay) added an explicit "Verifiability note" listing the exact commands so this re-verification is now part of the doc.
No change needed. Marking this finding as not-applicable against current main.
— sent from smart-boar-330
| - `src/v4/std/verification.dag` — `TestClaim` substrate (eval's downstream consumer). | ||
| - `src/v4/extdeps/languages/dag.dag` + `rust.dag` + `python.dag` + `go.dag` + `cpp.dag` + `typescript.dag` — Wave-1 LanguageModels with Practice-8 fact-bundles. | ||
| - `src/v4/compiler/01_tokenize.dag`, `02_parse.dag`, `03_normalize.dag`, `03_resolve.dag` — pipeline scaffolds; T-8 implementation in flight. | ||
| - `src/v4/compiler/04_infer.dag`, `05_emit.dag`, `05_eval.dag`, `00_compile.dag` — scaffolds with correct interface shape, **bodies not implemented**. |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Valid finding against sha 77fe746, already addressed in commit f1306fb (pushed before this relay arrived).
The premise is correct: src/v4/compiler/00_compile.dag:50 declares fn compile(source: Source, target: TargetModel) -> Outcome<TargetSource>, which DOES diverge from this doc's ratified compile(source: CoreNode, input_lang: LanguageModel, mode: CompileMode) -> Outcome<Output>. The doc's prior "scaffolds have correct interface shape" claim was wrong on this point.
Fixed by:
- Removed the inaccurate "with correct interface shape" claim — updated the "What we have today" line for compile scaffolds to read "scaffolds with divergent interface shape — see 'Scaffold-vs-design divergence' below — and bodies not implemented."
- NEW "Scaffold-vs-design divergence — implementation migration plan" section that explicitly catalogs the six divergences (compile signature,
v4.lens.costimport in 04_infer.dag, missing canonical-grounding invariant, single-step emit vs P7 rewrite+coercion, eval as standalone vs translate-to-host, Source carrier vs CoreNode) and prescribes the migration. Implementation workers for T-9/T-10/T-22 land the ratified interface, not the stale scaffold.
This honors INVARIANTS P2: the doc no longer claims correct-interface-shape; the boundary discipline (substrate truthfulness) is restored, and the migration is named as the work-item.
— sent from smart-boar-330
…olf-435 review) Major doc amendment integrating the substantive review from PR #3437's sister doc (sunny-wolf-435 PM, against docs/design-read-edit-pipeline.md which merged in PR #3364 on 2026-05-19). Reviewer feedback was that the compiler-architecture doc had a substantial gap: it covered the COMPILE direction (text/data → target) thoroughly but was silent on the EDIT direction (CoreNode + Diff → CoreNode'), the read/edit pipeline merged in PR #3364, and the closely-related question "how will the compiler edit itself / regenerate stage0?" CHANGES: 1. NEW "Load-bearing references" section (after "What this document is"): Comprehensive list of foundational + adjacent ratified design docs the compiler architecture composes with. Includes THESIS / MODELING / modeling-discipline / INVARIANTS / TASKS as foundational, and 11 adjacent design docs (read-edit-pipeline, emit-stage-l25, infer-stage-l25, lens-application-surface, lens-framework, affected-set-lens, dissolution-lens, v4-close-interrogation, v4-dag-rationale, pure-bootstrap-zero, substrate-lambda-calculus-grounding, bootstrap-fact-model) plus 6 lens-specific design docs. 2. NEW 9th substrate primitive: apply_diff - Path / Edit / Diff vocabulary ratified in PR #3162 (std/node.dag) - apply_diff scaffold in lens/application.dag (T-23) - The substrate is read/write-symmetric: reads via fold_node / apply_lens; writes via apply_diff - Primitive set is now 9 things (was 8); TL;DR + tally line updated 3. NEW "The EDIT direction — symmetric to compile" section: - Read/edit primitives table (Path, Edit, Diff, apply_diff, subterm_at, apply_lens, affected_set) - The seven-step read→edit pipeline from PR #3364 § 4 - Candidate-state pattern: gates run against apply_diff(dag, Diff), NOT the pre-edit graph. Same monotonic-facts invariant as P3's facts-flow-forward, applied to mutation. - EDIT direction = the "Query-driven rewrite" ingest path (cross-link to the ingest paths table) - Library-first agent surface (per read/edit doc § 6.10) — extended to apply to compile() too - Lens as (find, transform) convolution view; cross-ref to mechanical refactor hero case (f) in read/edit doc § 6.7b 4. NEW "Self-modification, stage0, self-edit" section addressing the reviewer's specific question: - Compiler reads its own source as CoreNode (same lens surface as user code; no special introspection) - Compiler writes to its own source via apply_diff (two paths: hand-authored Diff or mechanical-refactor lens) - stage0 regeneration is compile(self, dag, TranslateTo(rust)) — no special mode; the homomorphism mechanic applies identically - Candidate-state for self-modification safety — lenses gate the candidate; compiler cannot break itself silently - Implications: no new substrate needed; self-hosting is one specific compile invocation; hand-Rust-to-zero IS the loop closing. 5. Glossary expanded with Path / Edit / Diff / apply_diff / apply_lens / SectionRef / scope_in / candidate-state pattern / affected_set / self-edit-stage0 vocabulary. The compile + edit directions are now both represented in the doc. The two designs (this one + read/edit pipeline) compose cleanly — same CoreNode, fold_node, Diagnostic substrate; the read/edit doc owns the agent-surface mechanics, this doc owns the homomorphism architecture, both are the same nine substrate primitives at different angles. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Findings on PR #3437 from codex 2026-05-20T05:24:15Z, all addressed in this commit: FINDING 1 — Validate-then-compile gate not type-enforced. P3 commitment 6 said the project-mandatory wrapper preserves the "by construction" guarantee, but that was convention, not type-level enforcement. Updated to require Validated<Output>-style carrier discharged only by the wrapper; bare compile() now explicitly marked as internal/non-terminal (accessible to advanced consumers — lens framework, build tooling, self-edit — but NOT the everyday user surface). The wrapper-as-terminal pattern is invariant at the type level. FINDING 2 — Substrate inventory verifiability. The reviewer flagged "live-substrate inventory was not verified against the v4 tree." Verified refinement.dag IS on main (1143 bytes, status "T-25-core modeled" — landed via #3354); the doc claim was correct. Added a "Verifiability note" pointing at the verification commands (ls + head -10) + added commit refs (#3354 for refinement.dag, #3162 for Path/Edit/Diff vocabulary, #3436 for in-flight T-8 PR) so future reviews can verify independently. Also added lens/application.dag and lens/affected_set.dag to the inventory (they were missing). FINDING 3 — Scaffold-vs-design divergence. The reviewer correctly identified that the compiler scaffolds in src/v4/compiler/ predate this doc's ratifications and have divergent signatures (00_compile.dag's `compile(Source, TargetModel) -> TargetSource` vs this doc's `compile(CoreNode, LanguageModel, CompileMode) -> Outcome<Output>`, 04_infer.dag's `v4.lens.cost` import vs P3's no-named-lens rule, etc.). Added a "Scaffold-vs-design divergence — implementation migration plan" section that explicitly catalogs the divergences and prescribes the migration. The scaffolds are shape placeholders; implementation workers should land the ratified interface, not preserve stale signatures. NOT addressing as a separate finding — eager-bat-439 archive refused because PR #3436 is still open. Worker delivered cleanly (2 approvals, CI green, conflict markers resolved); operator manual squash-merge is the gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…regeneration substrate Integrates the operator's review per 2026-05-20 — two ratifications + named regeneration substrate. NEW PREMISE P8 — The compiler is not exempt from its own discipline: The compiler is itself a modeled system. Its layers (stages, language models, lenses, testgen, target models, diagnostics, glue derivation) are modeled as dependency graphs over the same substrate primitives. When an upstream model changes, the compiler computes the affected downstream subgraph (T-21 affected_set) and regenerates derivable artifacts; non-derivable consequences fail-closed. "No hidden anything" generalized: no implicit conventions, no manual synchronization, no hidden emitter / parser / test-generator / integration- updater / layer-specific-patcher / ad-hoc-Node-traversal-outside-primitives. Every compiler-internal artifact must be a substrate primitive OR a declared algebra OR a lens OR a projection OR a target/runtime policy. The slogan: the compiler is the first consumer of its own modeling discipline. If implementation workers find themselves writing ad hoc code to keep compiler layers in sync, that is a STOP condition. Two worked examples added under P8: - testgen self-regeneration: Refinement<T> shape changes → affected_set computes which TestClaims/TestCases/target test files regenerate → lens family re-fires automatically on the affected subgraph. - LanguageModel self-regeneration: LanguageModel gains a new field (e.g., effect-semantics per Q10) → affected_set computes which stages/lenses depend on it → each extends or fails-closed on the new field. NEW "Named regeneration substrate" section (under P8) cataloging the substrate concepts P0 + P8 need that are not yet declared: - ChangeSet (std/change.dag) - AffectedSet (T-21 is the lens-frontier specialization; full version not yet declared) - Projection (std/projection.dag) - Artifact (std/artifact.dag) - RecomputePlan REFINED TESTGEN LENS FAMILY (per reviewer's three-layer taxonomy): - Layer 1: TestClaimLens — InferredTree → TestClaim Witnesses (abstract behavioral claims: roundtrip / refinement-boundary / algebra-law / protocol-compat / effect-idempotency) - Layer 2: TestCaseLens — TestClaim Witnesses → TestCase Witnesses (concrete cases: examples, boundary cases, property-test generators, fuzz seeds, regression fixtures) - Layer 3: TargetTestProjection — TestCase Witnesses + target LanguageModel → target test source (Rust #[test], pytest, Jest, integration harness) Profile invocations expanded with reviewer's full taxonomy: smoke, boundary, property, algebra_law, effect, integration, roundtrip, equivalence, fuzz, regression. All share std/verification.dag (landed) + std/refinement.dag (landed) + std/dependency.dag (P6 substrate, not yet declared) + std/testgen.dag (renamed from lens/testgen.dag, follow-up bookkeeping). Self-regeneration cross-reference: when a model fact changes, affected_set computes which testgen lenses re-fire on which subgraph — no manual sync. GLOSSARY EXPANDED: TestClaimLens, TestCaseLens, TargetTestProjection, ChangeSet, AffectedSet, Projection, Artifact, RecomputePlan. The compiler architecture now has the full mental model: - Semantic substrate: 6 connectives + 5 behaviors - Compiler substrate: 9 primitives (fold_node, traverse, grammar-as-data, solve_constraints, coercion fold, LawfulRewriteWitness, dep graph, apply_diff, diagnostic+locus) - System substrate (not yet declared): ChangeSet, AffectedSet, Projection, Artifact, RecomputePlan - Derived outputs: target code, eval values, tests, dim facts, glue, diagnostics, and compiler artifacts themselves (P8) The big idea: v4 does not merely compile .dag programs. v4 models systems — including itself — as dependency graphs, then regenerates all downstream projections when upstream facts change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
174f9704· Trigger:schedule - Thinking:
264s wall
BLOCKING (3)
Root Cause
docs/design-v4-compiler-homomorphism.mdP8 collapsed the lens-frontier affected_set specialization into the broader projection-regeneration substrate → make P8 name the generic ChangeSet/AffectedSet/Projection/RecomputePlan contract and describe T-21 as only the lens-frontier specialization.docs/design-v4-compiler-homomorphism.mdThe model-evolution contract does not distinguish schema-declared safe defaults from unknown missing facts → require diagnostics for missing required facts and allow defaults only when the field schema carries a sound default witness.docs/design-v4-compiler-homomorphism.mdThe self-hosting example retained the pre-separation text pipeline → split it into ingest_text(...)->CoreNode or preexisting self CoreNode, then compile(CoreNode, dag_lang, TranslateTo(rust_lang)).
|
|
||
| The v4 compiler must receive the same structural benefits it provides to user programs. **Compiler stages, language models, lenses, test generation, target models, diagnostics, and glue derivation are themselves modeled as dependency graphs over the same substrate primitives.** | ||
|
|
||
| A change to an upstream model — Node shape, grammar productions, `LanguageModel`, `ModelCore`, dependency kind, lens contract, coercion-fold witness shape, or `HostModel` — must produce a `ChangeSet`. The system computes the affected downstream compiler artifacts (via T-21 `affected_set`) and regenerates them where derivable. If a downstream artifact cannot be regenerated from the updated model, the compiler **fails closed** with an explicit diagnostic. |
There was a problem hiding this comment.
BLOCKING: INVARIANTS P2 boundary discipline: P8 makes T-21 affected_set the mechanism for arbitrary compiler-artifact regeneration even though the required ChangeSet/AffectedSet/Projection/RecomputePlan substrate is separately undeclared, leaving regeneration authority split.
There was a problem hiding this comment.
Valid finding. Resolved in commit f0e125a.
The 'Named regeneration substrate' section now explicitly states the substrate must land as a unified coherent declaration, not piecemeal. T-21 affected_set is a specialization (lens-frontier only) of the general AffectedSet, and the two MUST unify — split authority is itself a P2 violation. Implementation order updated: declare the regeneration substrate as a unit (std/regeneration.dag or tightly-related cluster); T-21 affected_set will be MIGRATED into the unified shape, NOT maintained as a parallel concept.
— sent from smart-boar-330
|
|
||
| 1. `affected_set` computes which compiler stages / lenses depend on `LanguageModel`'s shape (resolve consults binding rules; ground consults inhabitance; translate consults grammar; …). | ||
| 2. Each affected stage's algebra extends or fails-closed on the new field. | ||
| 3. Existing `rust.dag` / `python.dag` / etc. fail-closed-or-default on the new field until updated. |
There was a problem hiding this comment.
BLOCKING: INVARIANTS P3 fail-closed: fail-closed-or-default allows missing newly-required LanguageModel or ModelCore facts to be accepted by default without requiring a typed default witness or diagnostic.
There was a problem hiding this comment.
Valid finding. Resolved in commit f0e125a.
Removed 'fail-closed-or-default' from the language-model self-regeneration worked example. Replaced with explicit binary choice: missing newly-required facts produce either (a) a typed Default<T> witness declared as substrate data (modeled default, NOT implicit silent default), or (b) a fail-closed diagnostic. No silent default acceptance — per P3 fail-closed, the absence of a fact is either modeled (witness) or signalled (diagnostic), never accepted as a default by default.
— sent from smart-boar-330
| ) -> Outcome<TargetSource> // the emitted Rust bootstrap source | ||
| ``` | ||
|
|
||
| There is **no special "regenerate stage0" mode**. stage0 regeneration is a `TranslateTo(rust_lang)` compile where the input happens to be the compiler's own source. The homomorphism mechanic applies identically: parse + normalize + resolve + ground the `.dag` source; coercion-fold against `rust.dag`'s declared inhabitants; serialize via Rust's grammar. The output is the Rust bootstrap that THESIS facet 2 ("compiler self-emits, fixed-point") requires. |
There was a problem hiding this comment.
BLOCKING: INVARIANTS P2 boundary discipline: the stage0 self-compile path folds parse and normalize back into compile(...), contradicting this doc's ratified text/data separation where compile-core consumes CoreNode.
There was a problem hiding this comment.
Valid finding. Resolved in commit f0e125a.
The stage0-regeneration code block now shows explicit ingest_text + compile composition:
self_corenode = ingest_text(read_file('compiler.dag'), dag_lang) -> Outcome<CoreNode>
stage0_source = compile(self_corenode, dag_lang, TranslateTo(rust_lang)) -> Outcome<TargetSource>
Compile-core takes CoreNode (data), never text. ingest_text is the separable boundary action; compile is pure data-in / data-out. The 'no special regenerate stage0 mode' claim is preserved, but parse + normalize are NOT folded back into compile — they are explicitly the ingest layer per the text/data separation ratification.
Added 'Equivalent paths' note showing other ways to obtain the CoreNode (already-cached, programmatic builder, query-driven rewrite) — all funnel through compile() taking CoreNode, never through compile() taking text.
— sent from smart-boar-330
…elf-modifying code Integrates the reviewer's critical clarification (2026-05-20): "compiler edits itself" is loose; the precise framing is "compiler models itself; generates candidates; promotion is guarded." Resolves the architectural ambiguity in the prior self-modification framing without falling into v2's manual-stage0-patch failure mode OR free-runtime-self-modification (intractable). NEW PREMISE P9 — Bootstrap is stratified; stage0 is a generated artifact: The compiler may model and regenerate its own implementation, INCLUDING stage0, but no running compiler generation mutates itself in place. The compiler can DERIVE AND VERIFY a replacement stage0 from Stage0Spec; it cannot arbitrarily rewrite itself at runtime. THREE-PIPELINE FRAMING (must not collapse): 1. Semantic compile pipeline — text → InferredGraph → target/eval. 2. Artifact projection pipeline — InferredGraph → generated compiler code / tests / docs / schemas / glue / stage1 source. 3. Bootstrap promotion pipeline — current Stage0[k] + candidates → Stage0[k+1] (or rejection diagnostic), guarded by BootstrapWitness + FixedPointWitness. The mistake is collapsing all three into "the compiler edits itself." WHAT STAGE0 IS: - A minimal seed runner (NOT "the whole compiler but worse"). - Consumes a stable canonical CorePackage (NOT arbitrary evolving surface syntax). - Stage0Contract declares: load CorePackage; understand stable Node/Core schema; run minimal fold_node/traverse; fail-closed diagnostics; emit verified artifact. This decoupling is the structural answer to v2's pain — surface language / parser / normalizer / lenses can all evolve without breaking stage0 because stage0 consumes the canonical package, not the surface. BOOTSTRAP EPOCH LOOP: - Stage0[k] + CorePackage[k] → Stage1[k] - Stage1[k] + SourceModels[k] → Stage1'[k] - verify(Stage1[k] == Stage1'[k]) → FixedPointWitness[k] - Upgrade k → k+1: ChangeSet + AffectedSet + RecomputePlan → Stage0Candidate + Stage1Candidate → verify → promote. Only the promotion protocol replaces the active stage0. No back edge anywhere else. THREE CASES for compiler-contract changes: 1. Normal downstream (no stage0 impact) — affected artifacts recomputed. 2. Bootstrap-compatible stage0 change — current compiler generates Stage0Candidate; verify; promote. No manual edit. 3. Bootstrap-breaking change — requires modeled Bridge[k → k+1] migration package, or fails closed with BootstrapBreak diagnostic. CRITICAL INVARIANT: "At no point does an artifact become source of truth merely because it is needed for bootstrapping." Generated stage0.rs / compiler.corepkg / generated compiler source / generated tests are NOT authorities — they're disposable artifacts with witnesses. The source of truth remains .dag models + Stage0Contract + CorePackageSchema + Projection definitions. CONCEPTUAL STACK (Layer 0-4): - Layer 0: Seed (stage0 executable, minimal, audited, consumes CorePackage) - Layer 1: Substrate models (.dag, source of truth) - Layer 2: Compiler models (.dag, source of truth) - Layer 3: Generated compiler artifacts (disposable, regeneratable) - Layer 4: Verification / promotion (procedural and conservative gatekeeper) Only Layer 0 is hand-seeded. Layers 1-2 are source of truth. Layer 3 is disposable. Layer 4 is the gatekeeper. TWO DISTINCT DEPENDENCY GRAPHS (must be separated): - Program dependency graph (P6) — Contains / BindsTo / TypeDependsOn / DataDependsOn / EffectDependsOn / ResourceDependsOn / ModuleDependsOn / BarrierBefore / PlacementConstraint. - Build / bootstrap dependency graph (new) — ModelDependsOn / ProjectionDependsOn / GeneratedFrom / VerifiedBy / PromotedBy / BootstrapDependsOn. Keeping them separate prevents the confusion "does the compiler's own resolver depend on the resolver it is resolving?" — answer: at epoch k, Stage0[k] resolves model[k] enough to build Stage1[k]. No active stage depends on its own output. NEW BOOTSTRAP SUBSTRATE (P9 implies these; not yet declared): - Stage0Contract, BootstrapEpoch - CorePackage, CorePackageSchema - Bridge (migration package for bootstrap-breaking changes) - BootstrapWitness, FixedPointWitness - PromotionPlan, PromotionDiagnostic / BootstrapBreak Likely lands in std/bootstrap.dag alongside P8's regeneration substrate (ChangeSet / AffectedSet / Projection / Artifact / RecomputePlan). WHAT THIS RULES OUT (STOP conditions for implementation workers): - Code letting stage0 directly edit itself at runtime. - A "bootstrap workaround" that hand-edits stage0 outside the candidate / promotion path. - A "we know this is safe" that skips fixed-point verification. - Generated-artifact files treated as authorities. UPDATED EXISTING SELF-MODIFICATION SECTION to cross-reference P9 and clarify that the "compiler edits itself" framing is loose; the precise mechanic is candidate generation + verification + promotion. GLOSSARY EXPANDED: Stage0Contract, CorePackage / CorePackageSchema, BootstrapEpoch, Bridge, BootstrapWitness / FixedPointWitness, promotion protocol. The "fractal feeling" of self-application is now resolved structurally: the pattern is stratified (Layer 0 → Layer 4), not infinitely recursive. Only the model layer is source of truth; the bootstrap layer is intentionally tiny; the promotion layer is procedural; the artifact layer is disposable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Findings on commit b1cfdb8 (codex 2026-05-20T06:44:32Z): FINDING A (3271748181) — P2 boundary discipline: T-21 affected_set as specialization vs full AffectedSet undeclared = split regeneration authority. Fix: clarified in "Named regeneration substrate" section that these substrate concepts must land as a UNIFIED coherent declaration (std/regeneration.dag or tightly-related cluster), not piecemeal. T-21's affected_set must be MIGRATED into the unified AffectedSet — not left as a parallel concept (which would itself be a P2 violation). Implementation order updated: declare the regeneration substrate as a unit; migrate T-21 into the unified shape. FINDING B (3271748191) — P3 fail-closed: "fail-closed-or-default" wording in the language-model self-regeneration worked example allowed silent default acceptance of missing newly-required facts. Fix: removed "fail-closed-or-default". Replaced with explicit choice — either (a) a typed Default<T> witness declared as substrate data (modeled default, NOT implicit silent default), or (b) a fail-closed diagnostic. No silent default acceptance — per P3, missing newly-required facts produce typed witness OR diagnostic, never unsignalled default. FINDING C (3271748200) — P2 boundary discipline: stage0 self-compile path appeared to fold parse + normalize back into compile(...), contradicting the text/data separation where compile-core consumes CoreNode. Fix: rewrote the stage0-regeneration code block to show explicit ingest_text + compile composition. Compile-core takes CoreNode (data), never text. ingest_text is the separable boundary; compile is the pure data-in / data-out core. Added "Equivalent paths" note showing other ways to obtain CoreNode (already-cached, programmatic builder, query-driven rewrite) — all funnel through compile() taking CoreNode. The "no special regenerate stage0 mode" claim is preserved (stage0 regeneration is still compile(self_corenode, dag, TranslateTo(rust))) but the ingest boundary is now explicit and separable. v2's manual-patch failure mode is structurally precluded by the ratified text/data separation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Operator-direct refinement: the "shim/modeling thing extends to reads/writes
as well." The architecturally pure approach models files, file_system, shell,
and OS independently in extdeps/; all I/O is modeled effects against modeled
resources; compile-core has no boundary actions.
CHANGES:
1. TL;DR boundary actions reframed:
FROM: "Compile-core boundary actions: write output text (or execute),
report diagnostics. Two actions; compile-core is otherwise pure data-in /
data-out. Ingest-layer boundary actions (separable): read input text only
when ingesting from a text source."
TO: "Compile-core has no boundary actions. The compile core is purely
data-in / data-out. All real-world I/O — reading source from disk,
writing target source to disk, executing on a host, reporting diagnostics
to stderr — is modeled as effects against modeled resources
(extdeps/file_system.dag for files, extdeps/process.dag for shell/OS,
extdeps/network.dag for network), composed by peripheral shims outside
the compile-core surface."
2. End-to-end I/O section rewritten:
- Removed ingest_text from the public substrate primitive signature.
- Added explicit "Peripheral shims for text and file I/O" subsection
showing the composition: file_read (modeled effect) + ingest_text (shim)
+ compile (pure) + file_write (modeled effect) — each step is its own
substrate-modeled operation, NOT a compile-core boundary action.
- Added "Why this matters architecturally" — no hidden side effects;
dry-run works as composition; incremental rebuild works because every
artifact's provenance is modeled; self-modification is safe because
apply_diff is modeled, not implicit.
- Slogan: "No implicit I/O. Files are not the architecture. Effects are
modeled, not assumed."
3. Glossary added:
- peripheral shim — user-facing convenience composing modeled effects
with compile-core; NOT a substrate primitive.
- modeled effect — real-world I/O declared as substrate data in extdeps/
carrying EffectDependsOn / ResourceDependsOn edges; visible to lenses;
substitutable for dry-run.
This sharpens P0 + P8 + P3-dry-run: there are no implicit side effects
anywhere in the architecture. Files are orthogonal to the architecture;
they're modeled in extdeps/file_system.dag, NOT load-bearing for compile.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Review against the read/edit pipeline design (PR #3364, merged on main as
|
…routes
Four targeted tightenings before this wave of worker dispatch:
1. NEW "Terminology" subsection before P5: catamorphism / homomorphism /
coercion are three terms at three levels (mechanism / noun / verb).
The coercion fold is a catamorphism whose job is to verify a homomorphism.
Translation IS the homomorphism (the noun); coercion is the
verification verb. Doc passages conflating "coercion fold" with
"homomorphism mechanic" generically are sloppy and should be flagged.
2. Coercion fold primitive description now names the TranslatePlan
extension slot: conceptually
TranslatePlan = ExactCoercion(source_grounding, target_node)
| RewrittenThenCoerced(rewrite_witness, ...)
MVP implements only ExactCoercion; future LawfulRewriteWitness (P7)
lands the second variant without refactor.
3. Artifact carrier (in the regeneration substrate) now reserves
bootstrap-related ArtifactKind variants up front: Stage0Candidate,
CorePackage, WitnessBundle. Lets P9 bootstrap substrate land later
without forcing artifact/projection refactor.
4. NEW "MVP routes — named explicitly" section before "What's NOT in scope":
- Core MVP: compile-core homomorphism produces TargetSource from CoreNode
- MVP-A (translate-only): Core MVP + file_system shim → file-to-file
- MVP-B (eval-only): Core MVP + host_model + T-22 → Value
Either MVP-A or MVP-B is sufficient as the first proof point;
both together is the strongest exercise.
The terminology section is the key piece — operator + reviewer were
unclear on whether we were moving from coercion to homomorphism; the
answer is they coexist at different levels and the doc should use them
precisely. The other three are scope-reservation moves that prevent
future refactor when held substrate (LawfulRewrite, bootstrap, multi-lens)
eventually lands.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Thanks for the review against the read/edit pipeline doc. All six recommendations are already addressed in the current doc state (commits
Beyond the six items: the doc has also been extended with P8 (compiler obeys its own discipline) and P9 (stratified bootstrap) — the "compiler edits itself" axis the review raised as missing is now treated explicitly. The precise framing is that the compiler models itself and generates a candidate next-compiler as an artifact; the active running compiler does NOT mutate itself in place. stage0 regeneration is a self-targeting compile invocation, with the candidate-state + verification + promotion protocol from the read/edit pipeline doc as the safety mechanism. The two designs now compose explicitly. If sunny-wolf-435 wants to re-review against the current state, the relevant sections are:
— sent from smart-boar-330 |
Re-review at HEAD
|
| Prior concern | Now addressed at |
|---|---|
No reference to PR #3364 / design-read-edit-pipeline.md |
Lines 29–30 as load-bearing adjacent reference: "the EDIT-direction companion to this doc" |
No apply_diff / Path / Edit / Diff vocabulary |
Line 104 + line 622 substrate-operations table + line 762 EDIT-direction section |
| No EDIT-direction section | Full section starting line 760 ("The EDIT direction — symmetric to compile") |
| No seven-step read→edit pipeline | Quoted at line 776+ with the candidate-state framing |
No scope_in(root, ref) helper |
Line 794 with the candidate-vs-pre-edit rationale |
| No library-first agent surface | Line 802+ ("All substrate primitives surface as library functions") |
| No (find, transform) convolution view / mechanical refactor hero case | Line 812+ explicitly references "§ 6.7b (f) mechanical refactor" + the PR #3338 canonical-B worked example |
| No "how does the compiler edit itself" answer | Entire "Self-modification, stage0, self-edit" section (line 915+), which explicitly calls out "the specific question the read/edit doc reviewer raised" |
| No stage0 architecture / self-host story | P9 ratified ("Bootstrap is stratified; stage0 is a generated artifact, not self-modifying code"), three-pipeline distinction, k-epoch bootstrap loop, three cases for compiler-contract changes, critical invariant on artifacts-never-being-source-of-truth |
What I think the revision gets right (substantive)
- The three-pipeline distinction (P9) — separating Semantic Compile / Artifact Projection / Bootstrap Promotion. Naming the failure mode of collapsing them ("compiler edits itself" framing as loose) is the clarity v2 lacked.
- CorePackage as the stable bootstrap interface. Stage0 consumes a canonical package, not the full evolving surface. This structurally prevents the v2 pain mode ("stage0 must understand the same evolving contracts → constant manual patch pressure"). Directly addresses the substantive concerns from sunny-otter-371's stage0-independence work (PR #3407).
- Three cases for compiler-contract changes (normal / bootstrap-compatible / bootstrap-breaking) — concrete decision table, including fail-closed
BootstrapBreakdiagnostic for the breaking case. - Critical invariant: "At no point does an artifact become source of truth merely because it is needed for bootstrapping." This is the right discipline statement.
- Stage0 regeneration as a uniform
compile()call:compile(self_corenode, dag_lang, TranslateTo(rust_lang))— no special "regenerate stage0" mode. Same uniform composition. This is structurally honest. - Candidate-state for self-modification safety with concrete lens-gate code example. The "compiler cannot break itself silently" claim is now substantiated by the explicit lens-gate framework.
Minor remaining points worth considering (not blockers)
These are small; the doc is substantively ready:
- The
Stage0Spec/Stage0Contract/CorePackageSchematypes are referenced but their concrete shapes aren't sketched. This may belong in a follow-up substrate brief (it's a real design question — what fields doesStage0Contractcarry?) rather than this architecture doc, but worth deciding whether to in-line a sketch or explicitly defer. - The relationship between
BootstrapWitness,FixedPointWitness,LawfulRewriteWitness, andWitness<homomorphism>(from P7) — these are all "witnesses" but for different things. A brief witness-taxonomy paragraph would help readers reason about which witness goes where. - The bootstrap epoch loop's
Bridge[k → k+1]migration package — when does the bridge itself need a bridge (when does upgrade-the-bridge become a bootstrap-breaking change)? Probably a Q-row in the open-questions section, since it's the second-order question. - Cross-link to sunny-otter-371's PR v2 stage0 independence — investigation (analysis-only, no implementation) #3407 specifically in the P9 section — that work surfaced the empirical "stage0 mirror is fundamentally broken" finding that motivated this stratification design. Citing it would close the loop on attribution.
Net read
The revision is substantive and the doc is now genuinely composable with the read/edit pipeline. The "how will the compiler edit itself" question is answered both at the operational level (apply_diff + candidate-state + lens-gate) and at the architectural level (P9 stratification + bootstrap promotion protocol). My prior review is superseded.
— sent from sunny-wolf-435
|
Thanks for the thorough re-review + the explicit supersede. Addressed all four non-blocker minor points in commit
All four are surgical (~30 lines net) and tighten without changing architectural commitments. Appreciate the substantive review. — sent from smart-boar-330 |
…ied Q1 + P4) PR #3437 (commit deda6f2) ratified three substrate concepts in `docs/design-v4-compiler-homomorphism.md` that had no TASKS.md home: - **Ratified Q1 (2026-05-20)** — `HostModel` is a distinct peer of `LanguageModel`, both extending a shared `ModelCore`. Files needed: `std/model_core.dag` + `std/host.dag` (neither exists on main). - **P4 (2026-05-20)** — Glue derivation is a composed homomorphism; `extdeps/protocols/` is named verbatim as "Currently missing" substrate (REST / GraphQL / gRPC). Adds three rows: - **T-33** `std/model_core.dag` — shared substrate factoring [needs T-1, T-2, T-3] - **T-34** `std/host.dag` — HostModel peer of LanguageModel [needs T-33] - **T-4.15** `extdeps/protocols/{rest,graphql,grpc}.dag` — transport substrate, P4 [needs T-3, T-26, T-4]; out-of-scope for initial single-target compiler, in-scope so glue derivation isn't foreclosed Plus the parallel-fill execution-graph block at top of file is updated to list the three new rows. No new doc, no anemia-audit work, no Wave-1 LanguageModel fleshout — T-30 owns the structural anemia gate, T-4 owns the fact-bundle rework, and `docs/audit/coproduct-anemia-inventory.md` is the existing one-shot census. The catalogue-doc shape the original brief proposed collided with the operator's standing ledger principle (CLAUDE.md, 2026-05-19); this PR is the narrower form the operator ratified instead — three TASKS.md rows, zero new docs. T-4's `[needs …]` is intentionally NOT edited here. Once `model_core.dag` lands, the T-4 fact-bundle authoring contract should be re-expressed in terms of "LanguageModel extends ModelCore" — that reconcile is its own commit train, not bundled with the substrate landing. The Q1 ratification established the SHAPE; landing the carrier file and re-routing T-4's authoring are two separable steps. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Addresses two of the three codex findings on PR #3442 (BLOCKING): - **T-33 → T-4 edge.** Reviewer correctly observed that T-33's body claims "consumed by T-4 (LanguageModel)" but T-4's `[needs …]` contract omitted T-33 — so LanguageModel could be scheduled before its shared substrate facts exist. Fix: add T-33 to T-4's `[needs T-3, P1-KEYSTONE, T-29, T-30, T-25-core, T-33]` in both the side-branch graph block (top of file) and T-4's task-definition body. Side-branch graph + feeders block updated to four → five feeders. T-33's own task body unchanged. - **T-34 → T-22 edge.** Same shape — T-34's body claims "Consumer: T-22 eval + MVP-B route" but T-22 still needed only T-9. Fix: T-22's parallel-fill execution-graph entry now `[needs T-9, T-34]`, with a one-line note pointing at the Ratified Q1 origin. NOT done in this commit (deliberate): - **T-22's task-definition body signature `eval: (InferredTree, Inputs)`** is not updated to include the HostModel parameter. Adding the graph edge records the dependency; restructuring eval's signature is a substantive modeling change and stays a separate commit train. - **T-4's body text on "fact-bundle authoring contract"** is not re-expressed in terms of "LanguageModel extends ModelCore". Same reasoning — graph edge ≠ authoring-contract reconcile. The third codex finding (`docs/design-v4-compiler-homomorphism.md` absent at PR head) is a false positive — the bot reviewed `fecd3bd0` (the WIP snapshot) and reported the file as missing, but the file landed in `deda6f210` (PR #3437) on main 2026-05-20 03:23 and is present at every commit on this branch. Blob hash `6afcb0914dbf3884b687ab7f3696b00dbacf1fa2`, 1333 lines, verified at PR head + origin/main + origin PR branch. Reply on that thread, no fix commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…e unification (#3443) * design: Pass A + Pass B amendments — strict simplification + primitive unification Follow-on to merged PR #3437 (architecture doc). Two-pass strict-mode amendment per operator-direct audit 2026-05-20. PASS A — concrete violations (3 fixes): 1. Strip Lossy from CoercionQuality lattice (P3 fail-closed violation). - TASKS.md T-9 lines 419-420: CoercionQuality = Identity | Exact only. Lossy operations are explicit user-declared source operations (floor / int_truncate / widening_cast), not a coercion-time category. Loss is a diagnostic via CoercionMismatchKind, NOT a success-with- warning. - Architecture doc primitive table reflects the strip. 2. Strip TranslatePlan.RewrittenThenCoerced extension slot (P2 illegal-states-unrepresentable violation — pre-emptive extension slot for unbuilt LawfulRewriteWitness was constructible). 3. Collapse three named MVPs (Core / MVP-A / MVP-B) → one MVP (P2 multiple-terminuses-for-one-boundary). MVP is: compile(corenode, dag_lang, TranslateTo(rust_lang)) for the add(x, y) = x + y worked example. Other endpoints are deferred-with-trigger. PASS B Part 1 — Open Q resolutions independent of unification: Ratified: Q7 (LanguageModel declarative-only), Q8 (CoercionMismatchKind diagnostic), Q11 (per-stage Outcome policy + 2-variant shape), Q12 (parse(serialize(node))==node grammar law), Q14 (target selection deterministic policy OR ambiguity diagnostic). Deferred-with-trigger: Q10 (effects/partiality — first effect-typed primitive), Q13 (versions/dialects — first multi-version case). PASS B Part 2 — Primitive unification (9 → 5) + witness collapse (7 → 3): NEW unified primitive find_witness(source_facts, closed_candidate_set, preservation_predicate) -> Outcome<(Candidate, Witness)> unifies: - solve_constraints (constraint-satisfaction predicate) - coercion fold (exact-structural-equality-zip-fold predicate) - LawfulRewriteWitness (lawful-rewrite-precondition predicate, P7) All three are find_witness invocations with different predicates. Derived combinators (no longer primitives): - traverse_node / sequence_node / bind_outcome = fold_node + Outcome- threading algebra. Combinator interprets StageDiagnosticPolicy as the single failure-handling authority. - apply_diff = fold_node(root, substitute_at_paths(diff)). - coercion fold / solve_constraints / LawfulRewriteWitness = derived from find_witness. Final substrate primitive set (5): 1. fold_node (root primitive) 2. Grammar-as-bidirectional-data 3. find_witness (unified search/check) 4. Typed dependency graph (with reason + subject, not just kind) 5. Diagnostic + Locus carrier WITNESS COLLAPSE (7 → 3 generic carriers): - StructuralPropertyWitness<P>: was CanonicalGroundingWitness + AcyclicityWitness + ClosedWorldDependencyWitness. - HomomorphismWitness<R>: was Witness<homomorphism> + LawfulRewriteWitness. - PromotionWitness: was BootstrapWitness + FixedPointWitness. Carriers parameterized by what they witness (property P / rule R), not by which primitive produced them. All checkable substrate data (per Ratified Q9 — derivation untrusted, witness check trusted). RATIFIED Q6 + Q9 (Pass B unification side-effects): - Q6 (multi-lens execution): derives from fold_node + composed-lens- algebra; no new primitive. Composed algebra topologically orders the lens-dependency DAG; single-pass traversal stages per-Node steps. - Q9 (witness checking): all 3 witness carriers support verify_witness re-check without re-running their producing primitive. PASS SUMMARY: - Substrate primitives: 9 → 5 - Witness types: 7 → 3 - Premises: 10 unchanged (P0-P9) - Open Qs: 15 → 0 (5 ratified in Pass A/B, 8 deferred-with-trigger, 2 absorbed into unification — Q6 + Q9). The doc shrinks meaningfully not by trimming prose, but by the underlying architecture being smaller — concept unification rather than aggressive prose-cutting (per operator guidance: qualitative, not line-count). This completes the architecture audit. Worker corrections round (swift-dove-578's coordination) follows once this lands on main. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address openai-pro REQUEST_CHANGES + codex BLOCKING Both reviewers identified the same root pattern: Pass B's primitive unification was applied to TL;DR/primitive table/glossary but not propagated to all authoritative sections, leaving conflicting active authorities. CODEX BLOCKING — P5/P7/Q4/MVP dispatch sections reconciled: - P5 (Fold discipline) — Practical implications rewritten so solve_constraints, coercion fold, and LawfulRewriteWitness are explicitly named as find_witness invocations with different preservation predicates. Same primitive, three predicates. - P7 (LawfulRewriteWitness) — Pipeline diagram + carrier description reframed to use find_witness with lawful-rewrite-precondition predicate. HomomorphismWitness<R> with different R values for exact-equality vs lawful-rewrite. Historical naming preserved per T-9 ratification. - Q4 (traverse_node) — Updated to mark traverse_node / sequence_node / bind_outcome as DERIVED from fold_node + Outcome-threading-algebra (not separate primitives). Incorporates Worker C's NodeOutcomeFold.step single- authority fix; combinator owns policy, algebra is pure-success-accumulator. - MVP dispatch entries — W-CoercionFold + W-TraverseOutcome reframed as find_witness/fold_node invocations with specific algebras-as-data, not separate primitive-implementation work items. Outcome migration named explicitly as Worker C corrected scope (not "corrections round" debt). OPENAI-PRO REQUEST_CHANGES — substrate authority conflicts resolved: 1. Outcome<T> shape — three sites (TASKS.md:419, Q8, Q14) used the legacy Produced/Rejected{diagnostic} singular shape. All three updated to ratified Q11 two-variant: Accepted{value, diagnostics: Diagnostics} | Rejected{diagnostics: NonEmptyDiagnostics}. CoercionMismatchKind carried as payload inside the diagnostic list, not as direct field. 2. Multi-lens primitive dissolved-and-deferred contradiction — MVP out-of-scope line replaced. Was "Multi-lens dependency primitive (Open Q6)" which contradicts Ratified Q6's "no new substrate primitive" stance. Now "LensAlgebra<F> carrier shape + composed-lens-algebra construction" — names the actual remaining substrate work without resurrecting the dissolved primitive framing. 3. DECISIONS ledger reference — TASKS.md:404 "DECISIONS §CP-1b item 2" replaced with "per CP-1b/T-8 dispatch row above and merged T-8 closeout PR #3436" (cite live authority per CLAUDE.md ledger standing principle). 4. Outcome reconcile as bounded scope (not informal "corrections round" debt) — primitive set table's Diagnostic+Locus row now explicitly names the 43-callsite migration as Worker C's corrected scope (one PR, one substrate authority), not vague future bucket. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address codex REQUEST_CHANGES — strip "search" framing from find_witness Codex (sha 264cd2b) flagged that find_witness was described as a "structure-preservation-search primitive" at lines 99 and 638, which contradicts T-9's explicit ratification ("not a search, not research" / "never call it a search algorithm"). Valid finding — fixed. CHANGES: 1. Line 99 (TL;DR): replaced "search-structure-preserving primitive" with "unified candidate-enumeration-and-check primitive". Explicit disclaimer added: "NOT a search, per src/v4/TASKS.md T-9 ratification." The word "find" in the operation name denotes the OUTPUT (canonical candidate or diagnostic), not a search algorithm. 2. Line 638 (primitive set table): replaced "THE structure-preservation- search primitive" with "THE unified candidate-enumeration-and-check primitive". Same NOT-a-search disclaimer. Description now explicitly uses "mechanically enumerates the candidate set and checks the preservation predicate" — closed enumeration + mechanical check, not heuristic search. Both updated descriptions consistent with T-9 ratification: closed candidate set + decidable-by-construction predicate + mechanical enumeration. The unification still holds (solve_constraints + coercion fold + LawfulRewriteWitness all derived); the framing now correctly emphasizes mechanical enumeration rather than search. Other uses of "search" in the doc are deliberate disclaimers / negations (e.g., "not heuristic search", "never call it 'search'") and are correct as-is. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: strip remaining "search" descriptor in glossary (codex RC followup) One additional glossary line at 1333 still had "THE structure-preservation- search primitive" — same problem as lines 99 and 638 (now fixed). Reworded to "candidate-enumeration-and-check primitive" with explicit NOT-a-search disclaimer per T-9 ratification. Final sweep: no "structure-preservation-search" or "search-structure- preserving" descriptors remain on find_witness anywhere in the doc. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address openai-pro REQUEST_CHANGES on sha 264cd2b Two internal contradictions that openai-pro correctly flagged: FINDING 1 — StageDiagnosticPolicy authority contradiction: - Q4 (line 1187) said "Single authority (lives in std/diagnostic.dag extension, NOT split across std/pipeline.dag)" - Q11 (line 1259) said "declared per stage in std/pipeline.dag" - These read as contradictory split authority. FIX: clarified that the TYPE declaration lives in std/diagnostic.dag (single authority); each stage row in std/pipeline.dag carries a diagnostic_policy: StageDiagnosticPolicy FIELD referencing per-stage values of that type. One type home, many per-stage values — not split authority, just type-vs-value distinction. Updated both Q4 and Q11 language to be consistent on this point. FINDING 2 — map_node_outcome reintroduced after being forbidden: - Q4 line 1185 forbids map_node_outcome as duplicate of bind_outcome (per Worker C finding #3) - Q11 line 1266 reintroduces map_node_outcome as a combinator threading StageDiagnosticPolicy FIX: Q11 list updated to use the canonical Q4 set — traverse_node / sequence_node / bind_outcome. map_node_outcome explicitly forbidden again in Q11; use bind_outcome instead. Both fixes are internal-consistency cleanups; no architectural change. The substrate plan now reads as one coherent design across Q4 + Q11. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: restore CI emit-wall bridge tracked note (codex RC) Codex correctly flagged that my prior TASKS.md edit deleted the tracked "CI emit-wall bridge" scaffold dissolution record while the bridge scaffold itself is still live in main: - scripts/v4-bootstrap-resolve-posture-gate.sh (blob exists) - .github/workflows/ci.yml references V4_BOOTSTRAP_ALLOW_RESOLVE_POSTURE_BRIDGE - dsl/gunbc/ci_github_actions_workflow.dag references it Deleting the dissolution record without dissolving the scaffold is a P5 violation (Progress Is Dissolution — yellow must dissolve, not just be untracked) and a Practice 9 violation (no untracked scaffolds). The deletion was inadvertent — inherited from session/smart-boar-330's state when I created the new branch via `git checkout session/smart-boar-330 -- src/v4/TASKS.md`. The bridge note belongs on the planning surface as long as the scaffold is live; the dissolution trigger is "typed resolve- only compiler gate lands OR emit reaches `compiled:` on standard-8 without host SIGTERM." FIX: bridge note restored verbatim from main. The CP-1b bucket C note (my actual intended edit) is preserved alongside it; both are tracked items in T-8's planning surface. When the bridge scaffold actually dissolves (the named trigger fires), its tracked note dissolves with it — in the same PR that removes the script + ci.yml + workflow.dag references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address codex P2 single-authority — Q6 + apply_diff stale primitive framings Codex correctly flagged that the doc still names Open Q6 as a "multi-lens substrate primitive" and apply_diff as a "write-side primitive" — both contradict the Pass B unification's "5 primitives total" claim. Q6 STALE FRAMINGS (4 sites): - Line 256 (P3 commitment 5): "See Open Q6 for the substrate primitive" → "See Ratified Q6 below — derives from fold_node + composed-lens- algebra; NO new substrate primitive." - Line 267 (held-pending list): "multi-lens dependency-management primitive (Open Q6)" → "LensAlgebra<F> + composed-lens-algebra construction (per Ratified Q6 — NOT a substrate primitive; derives from fold_node)." - Line 598 (regeneration substrate impl order): "alongside or after the multi-lens dependency-management primitive (Open Q6)" → "alongside or after the LensAlgebra<F> + composed-lens-algebra substrate work (Ratified Q6 — derives from fold_node; NOT a separate primitive)." - Line 904 (testgen lens-to-lens deps): "Open Q6 multi-lens primitive" → "per Ratified Q6 — composed-lens-algebra derived from fold_node; NOT a separate primitive." APPLY_DIFF STALE FRAMINGS (3 sites): - Line 790 (EDIT direction intro): "apply_diff is the write-side primitive that mutates a CoreNode graph" → "apply_diff is the write-side derived combinator (post-Pass B unification — apply_diff = fold_node(root, substitute_at_paths(diff)), an instance of fold_node with the substitution algebra)." - Line 960 (self-edit explanation): "The substrate's read/write-symmetric primitive set means..." → "The substrate's read/write-symmetric mechanism (fold_node reads; fold_node-with-substitute_at_paths algebra writes) means..." - Line 1345 (glossary): "The structural-edit primitive symmetric to fold_node" → "(DERIVED, not primitive) The structural-edit derived combinator = fold_node(root, substitute_at_paths(diff))." Net: 7 doc passages now consistent with the "5 primitives total + derived combinators" claim from the primitive set table. P2 single-authority preserved: implementers cannot read this doc and conclude that multi-lens or apply_diff is a separate primitive. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: strip remaining stale multi-lens-as-primitive at line 1155 One additional site missed in the sweep: "Lens framework implementation" out-of-scope item still said "the multi-lens dependency-management substrate primitive remains Open Q6" — same stale framing as the other 4 sites fixed in c7cc9f7. Reworded to "the LensAlgebra<F> + composed-lens-algebra substrate work is ratified by Q6 (NOT a separate primitive; derives from fold_node)." Final scan now shows no remaining stale "multi-lens substrate primitive" references that aren't in negation/disclaimer contexts. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address cursor APPROVE_WITH_COMMENTS — 3 partial-unification slips cursor/composer-2.5 caught three partial-unification slips: 1. Line 790 vs 792-799 — apply_diff classified as derived at 790, but Read/edit primitives table at 792-799 still listed it (+ subterm_at / apply_lens / affected_set) under a "Primitive" column with primitive- level semantics. Split authority inside same doc. FIX: section title changed to "Read/edit vocabulary (substrate types + derived combinators)". Each row now marked as either "carrier type" (Path, Edit, Diff — substrate-data types) or "derived combinator" (apply_diff, subterm_at, apply_lens, affected_set — fold_node instances). Note at section head explicitly says these are NOT new primitives per the main primitive set table. 2. Line 1240 (Ratified Q9) — said "the compiler must not trust its own search/fold", contradicting the T-9-ratified "find_witness is not a search" discipline. FIX: replaced "search/fold" with "candidate-enumeration" — consistent with the rest of the doc's T-9-aligned framing. 3. Line 1338 (glossary ClosedWorldDependencyWitness) — Pass B witness taxonomy collapsed this into StructuralPropertyWitness<P>, but the glossary still defined it as a standalone witness. Risks Worker A implementing the old carrier name. FIX: glossary entry now annotated "collapsed into StructuralPropertyWitness<P> per Pass B witness taxonomy — instance with P = being-completely-classified." Same pattern as solve_constraints / coercion fold / LawfulRewriteWitness derived- instance annotations elsewhere in the glossary. Net: all three internal-consistency issues resolved. apply_diff is consistently derived everywhere; "search" language consistently disclaimed per T-9; witness collapse consistently applied in glossary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix apply_diff sequential semantics — substantive codex finding CRITICAL substantive finding from codex (sha b5d66eb): my apply_diff unification simplification was semantically WRONG. I had written apply_diff = fold_node(root, substitute_at_paths(diff)) — a single fold over the source with all paths substituted in parallel. But the read/edit pipeline doc requires SEQUENTIAL ordered semantics: - Each Edit applies to the current CANDIDATE state, not the original root. - Each subsequent Edit's Path resolves against the post-prior-Edit state. - Fail-closed if any Path doesn't resolve in the intermediate candidate. The "parallel substitution" framing would have lost the read/edit pipeline's per-Edit sequential resolution + fail-closed-on-intermediate- state semantics. P2/P3 violation. FIX: apply_diff reframed correctly across all 5 sites as: sequence_outcome(diff.edits, fn(edit, candidate) -> fold_node(candidate, substitute_at(edit.at, edit.replacement))) Composes fold_node + sequence_outcome (both derived combinators of fold_node). Each Edit applies to the *intermediate* candidate; sequential semantics preserved; fail-closed-on-unresolved-Path-in-intermediate-state preserved. 5 sites updated: - Line 104 (derived combinators in TL;DR) - Line 649 (derived combinators paragraph) - Line 790 (EDIT direction intro) - Line 801 (Read/edit vocabulary table) - Line 1347 (glossary entry) The unification still holds (apply_diff is derived from fold_node + sequence_outcome, not a separate primitive). The semantics are now correct: sequential per-Edit application, not parallel substitution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: fix Q6 scheduling-authority split — lens-dep DAG is a P6 instance Codex correctly flagged that line 1224 created a second scheduling authority: "composed-lens-algebra construction (which is itself a fold_node over the lens-dependency DAG)" — a parallel ordering authority to the Typed dependency graph + topological/SCC machinery primitive (P6's own ordering authority). P2 single-authority violation: TWO sites would own topological ordering — the typed-dep-graph primitive AND the lens-construction-fold. FIX: clarify that the lens-dependency DAG IS a typed dependency graph instance (per P6 — kinds like LensReadsLensOutput / LensRequiresFact), and its topological order is computed by the SAME P6 primitive (Typed dependency graph + topological/SCC machinery) that produces all program-level orderings. Composed lens algebra construction CONSUMES the topological order from that primitive — single scheduling authority, NOT a separate fold over the lens-dep DAG. Single authority preserved. The lens-dependency DAG is one of the typed-dep-graph primitive's consumer surfaces, not a parallel ordering mechanism. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix substrate-home contradiction find_witness vs predicate algebras Codex (openai-pro?) flagged that lines 638 + 1136 contradicted on where the predicate algebras live: - Line 638: find_witness primitive in std/find_witness.dag; predicate algebras in their consuming concept-homes (std/constraints.dag + std/coercion.dag). - Line 1136: find_witness primitive in std/find_witness.dag; predicate algebras also in std/find_witness.dag (replacing the separate files). Duplicate substrate authority — P2 violation. FIX: line 1136 reworded to match line 638. The find_witness primitive is generic and lives in std/find_witness.dag; the predicate algebras live in their consuming concept-homes per M10 (concepts get proper homes): - constraint-satisfaction predicate in std/constraints.dag - exact-structural-equality-zip-fold predicate in std/coercion.dag Worker B authors all three files (primitive + two algebras). Single authority per concept; primitive in find_witness.dag, predicates in their respective consuming files. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address openai-pro REQUEST_CHANGES — apply_lens glossary + find_witness ambiguity contract Two findings from openai-pro (sha e5a841a): FINDING 1 — apply_lens glossary entry stale. Line 1348 still defined apply_lens as "the substrate-level read-side primitive lenses use" — contradicts the reclassification of apply_lens as a derived combinator at line 803 ("read/edit vocabulary is NOT primitives"). P2 parallel-authority violation. FIX: glossary entry updated to "(DERIVED, not primitive) ... Derived combinator post-Pass B unification — fold_node with the lens's algebra; combinator owns StageDiagnosticPolicy (per Q4). Composes with fold_node, doesn't extend the primitive set." Matches the derived classification at lines 803 + 1146. FINDING 2 — find_witness "first match" dilutes ambiguity contract. Line 638 said "first match returns Outcome::Accepted; multiple matches return AmbiguousTargetCandidate" — but "first match returns" is an execution instruction a worker could faithfully implement while SKIPPING ambiguity detection. That would silently accept positionally-first candidates, violating fail-closed and Q14's "deterministic policy OR fail-closed-ambiguity" semantics. FIX: find_witness contract rewritten to require collecting ALL passing candidates before any acceptance decision: - Enumerate the ENTIRE closed candidate set; check predicate against EVERY candidate; collect ALL passing candidates. - THEN resolve: * Exactly one passing ⇒ Accepted. * Zero passing ⇒ Rejected(NoTargetCandidate). * Multiple passing ⇒ apply declared TargetSelectionPolicy (Q14); deterministic policy → Accepted(selected); no policy OR policy fails to disambiguate → Rejected(AmbiguousTargetCandidate). - NO positional-first-wins. Ambiguity detection is required. Fail-closed semantics preserved per Q14 + P3. Workers cannot faithfully implement a positional-first variant and pass review; the contract demands full enumeration before acceptance. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: TL;DR find_witness — remove 'first match wins'; match line 638 contract One more 'first match' reference missed in the prior sweep: line 99 (TL;DR) still said 'first match wins (or fail-closed when zero, ambiguity diagnostic when multiple).' That's the same positional-first problem as line 638 (already fixed). FIX: TL;DR description now matches line 638: collects ALL passing candidates before resolving; ambiguity detection required; no positional-first-wins. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: reconcile find_witness result shape to ratified Outcome record form (codex finding) codex flagged that line 638's find_witness contract still used positional Outcome::Accepted(candidate, witness) / Outcome::Rejected(NoTargetCandidate) spellings, contradicting the ratified two-variant record shape at line 640 + line 1263 + TASKS.md line 424: Outcome<T> = Accepted { value: T, diagnostics } | Rejected { diagnostics: NonEmptyDiagnostics } Two incompatible result shapes in the same design brief = single-authority violation (P2 / Practice 5). Implementers get conflicting API instructions at the exact primitive this PR is redefining. FIX: line 638 reworded to use the record/struct form throughout: - Accepted { value: (candidate, witness), diagnostics } - Rejected { diagnostics: NonEmptyDiagnostics { head: NoTargetCandidate {...}, ... } } - Rejected { diagnostics: NonEmptyDiagnostics { head: AmbiguousTargetCandidate { candidates }, ... } } with explicit parenthetical 'record/struct shape per Ratified Q11 — NOT positional variant constructors' to anchor the convention. Matches the existing record-shape spelling at line 1286. Verified by grep: no other Outcome::X(...) positional constructions remain in docs/design-v4-compiler-homomorphism.md or src/v4/TASKS.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: parameterize find_witness with caller-supplied MultiplicityPolicy (openai-pro finding) openai-pro flagged a substrate-contract bug: the generic find_witness primitive at lines 99 + 638 specified 'multiple ⇒ apply TargetSelectionPolicy per Ratified Q14,' but Q14 is scoped to target COERCION ambiguity (target language declares the policy). The same find_witness primitive is also used by Ground/infer for solve_constraints, where the output is the canonical SOURCE grounding. Baking target-selection into the generic level would let a future worker faithfully implement 'apply TargetSelectionPolicy' in a source-grounding context where the contract should be 'canonical or diagnosed ambiguous' — silently accepting an ambiguous canonical grounding via target-model preference. P3 fail-closed violation + single-authority violation (modeling-discipline.md Practice 5). FIX: add MultiplicityPolicy as the 4th parameter to find_witness; caller supplies per use site. find_witness( source_facts, closed_candidate_set, preservation_predicate, multiplicity_policy: MultiplicityPolicy, // <-- new, caller-supplied ) -> Outcome<(Candidate, Witness)> MultiplicityPolicy = | UniqueOnly // exactly-one or fail-closed | TargetSelection(TargetSelectionPolicy) // Q14 — target coercion only | RewritePolicy(...) // P7 placeholder solve_constraints binds MultiplicityPolicy::UniqueOnly unconditionally (canonical source grounding — no target-preference notion) coercion fold binds MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) (Q14, target-coercion-specific) LawfulRewriteWitness will bind MultiplicityPolicy::RewritePolicy when P7 lands Updates touched (consistency sweep): - TL;DR (line 99) — primitive signature + caller-binding examples - Primitive table (line 638) — full contract with all three multiplicity cases - Derived combinators (lines 650-652) — each call site shows its policy binding - Substrate-home note (line 1136) — std/find_witness.dag carries MultiplicityPolicy type; per-caller policy bindings live in std/constraints.dag (UniqueOnly) and std/coercion.dag (TargetSelection) - Q14 ratification (line 1282) — explicit scope clarification: TargetSelectionPolicy goes inside MultiplicityPolicy::TargetSelection, supplied ONLY by the coercion fold call site; generic primitive does NOT bake it in - Glossary (line 1335) — signature updated to include multiplicity_policy Separates substrate-level multiplicity-policy authority (the MultiplicityPolicy type, lives with the find_witness primitive in std/find_witness.dag) from target-language-level target-selection authority (the TargetSelectionPolicy value, lives with each target LanguageModel). Two distinct authorities — neither collapsed into the other. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix fold_node landed-vs-planned algebra conflation (briansrls inline finding) briansrls flagged a P2 live-substrate/primitive-contract split at line 636: the design said the landed fold_node algebra is fn(R, Edge, Node) -> Outcome<R> (pure-success-accumulator) but src/v4/std/node.dag line 43 shows the actual landed NodeFold<R> as init: fn(Node) -> R step: fn(R, Edge, R) -> R (pure catamorphism — no Outcome) These are not the same shape. The landed step is a true catamorphism combiner: takes the accumulator, the edge, and the ALREADY-FOLDED child result R. The doc was describing the planned NodeOutcomeFold DERIVED combinator (Worker C escalated signature-collapse) as if it were already landed at the primitive level. This created two problems: 1. P2 boundary discipline — doc-claim contradicts on-disk substrate. 2. Implementers reading the design would write algebras that don't typecheck against the actual NodeFold<R> carrier. FIX (line 636 only): rewrite the primitive table entry to honestly separate landed-vs-planned: Landed primitive (NodeFold<R>): - init: fn(Node) -> R - step: fn(R, Edge, R) -> R -- pure catamorphism, no Outcome - lives in src/v4/std/node.dag line 43 Planned derived combinator (NodeOutcomeFold): - algebra: fn(R, Edge, Node) -> Outcome<R> -- pure-success-accumulator - combinator interprets StageDiagnosticPolicy - lives at the derived-combinator layer (Worker C scope) - lands as part of the 43-callsite Outcome-shape migration Outcome-threading is explicitly stated as NOT in the primitive — it lives in the derived NodeOutcomeFold combinator. This preserves the single-authority discipline (combinator owns failure policy) while honestly reporting the on-disk shape. Verified lines 103, 648, 1183 (TL;DR + derived-combinators + Ratified Q4) all describe the DERIVED NodeOutcomeFold combinator, not the landed primitive — they're correctly contextualized in their respective sections. Only line 636 conflated the two. Cross-checked: src/v4/std/node.dag lines 43-46 confirm landed shape. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address cursor APPROVE_WITH_COMMENTS — bootstrap-table + 3 staleness syncs cursor BLOCKING (lines 528-529): the bootstrap substrate table listed BootstrapWitness + FixedPointWitness as separate concepts to declare, directly below line 511's witness taxonomy collapse that explicitly folds both into PromotionWitness. Parallel authority in the same section (P2 / Practice 5). FIX (line 528, single row replaces two): PromotionWitness (composed gate; Pass B witness-taxonomy unification) - sub-field (a): bootstrap-roundtrip check — Stage0Candidate[k+1] produces Stage1Candidate[k+1] (was BootstrapWitness) - sub-field (b): fixed-point check — Stage1[k] compiles to itself (was FixedPointWitness) Internal sub-fields, not separate authorities; matches line 511. cursor exploratory observations (3 staleness syncs to keep the doc internally coherent post-Pass-B): 1. Line 523 — Stage0Contract description said 'fold_node + traverse'; updated to 'fold_node + derived traverse_node combinator' to match Pass B's derived-combinator framing. 2. Lines 478-480 (Layer 1 substrate stack) — listed traverse + coercion fold as substrate primitives. Updated to the post-Pass-B 5-primitive set (Node, fold_node, find_witness, Outcome/Diagnostic/Locus, grammar-as-data, typed dependency graph, change/artifact/bootstrap substrate) + an explicit 'derived combinators on top' line listing traverse_node / sequence_node / bind_outcome / apply_diff / coercion fold / solve_constraints. 3. Line 1328 (Practice 10 glossary) — said 'use a substrate primitive (fold_node, traverse, coercion fold)'. Updated to distinguish primitives (fold_node, find_witness) from derived combinators (traverse_node, coercion fold, solve_constraints, etc.) — still directs implementers to those instead of hand-rolling. No new content; just resolves three places where the unification's collapsed primitive set hadn't propagated. Internal consistency restored against the 5-primitive table at line 632. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: unify PromotionWitness wording across bootstrap sections Co-authored-by: Brian Searls <briansrls@users.noreply.github.com> * design: trivial doc-hygiene per cursor exploratory observations (APPROVE) cursor APPROVE verdict on PR #3443 noted two non-blocking doc-hygiene exploratory observations. Trivial fixes since I'm here. 1. Line 1169 — Q0 ratification body said the new substrate question it raises is 'Open Q6 — multi-lens dependency management.' But Q6 IS ratified in this same PR (Ratified Q6 at line 1218). FIX: updated to 'Ratified Q6 — multi-lens execution derives from fold_node with a composed-lens-algebra' — matches the actual Q6 ratification title at line 1218. 2. Line 1274 (Q12 ratification body) said 'Already in the primitive set table (line 636).' But after Pass B edits, the table header is line 636 and Grammar-as-bidirectional-data row is at line 639. Brittle line-number reference. FIX: replaced the line number with a stable section-relative reference: 'see the Grammar-as-bidirectional-data row under The primitive set — the things the compiler IS.' Robust against future line drift. No semantic change; pure doc-hygiene reconcile. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: openai-pro REQUEST_CHANGES — 3 substrate-contract fixes openai-pro flagged three internally-inconsistent contracts on the current head (sha 8c1e199). All three would cause an implementer to encode the wrong primitive surface. Fixed: 1. NodeOutcomeFold.step signature contradicted landed NodeFold<R> (lines 103 + 1185) The derived combinator section said the Outcome-threading algebra is fn(R, Edge, Node) -> Outcome<R>, but the landed primitive at src/v4/std/node.dag:43 has step: fn(R, Edge, R) -> R. Third parameter is the already-folded child R, not the raw Node. The Outcome-threading derived algebra should match the primitive step shape with Outcome wrapping ONLY — not change the parameter list. Otherwise the derived combinator isn't really a fold_node instance. FIX: both lines 103 + 1185 now say fn(R, Edge, R) -> Outcome<R> with explicit cross-reference to the landed NodeFold<R>.step shape at std/node.dag:43. Single authority preserved. 2. Glossary derived-call signatures dropped multiplicity_policy (lines 1340-1342) The primitive signature at line 1339 (1 row above) requires multiplicity_policy: MultiplicityPolicy as the 4th arg — that's the whole point of the openai-pro single-authority finding already addressed in 9a97376. But the glossary entries for solve_constraints / coercion fold / LawfulRewriteWitness directly below showed 3-arg calls without policy. Implementers reading the glossary first would copy the wrong shape and reintroduce the policy-ambiguity the unification was supposed to remove. FIX: glossary rows now name the 4th arg explicitly with caller- correct policy binding: - solve_constraints: MultiplicityPolicy::UniqueOnly (NOT optional, NOT defaulted; pass at call site) - coercion fold: MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) (sourced from target model per Q14; sole legitimate target- selection-policy leakage site) - LawfulRewriteWitness: MultiplicityPolicy::RewritePolicy(...) (gated on P7; documents future shape only — NOT in MVP) 3. MVP carrier required RewritePolicy variant while P7 deferred (line 1138 vs line 1149 / line 654) Line 1138 said the MVP std/find_witness.dag carrier must include UniqueOnly | TargetSelection(TargetSelectionPolicy) | RewritePolicy(...) variants and 'Worker B authors all three.' But line 654 says RewritePolicy is introduced when P7 lands, and line 1149 puts P7 out of MVP scope. Untracked premature substrate surface — would land a RewritePolicy variant with no consumer in MVP. FIX: line 1138 now scopes MVP variants to UniqueOnly | TargetSelection(TargetSelectionPolicy) ONLY. RewritePolicy(...) is explicitly NOT in MVP — it lands together with P7 lawful-rewrite work per the P7 trigger. Worker B authors three files; RewritePolicy is added at P7, not MVP. Verified: zero remaining 'fn(R, Edge, Node) -> Outcome<R>' references in the doc; all find_witness call shapes in the glossary now name multiplicity_policy explicitly with the correct per-caller binding. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: PromotionWitness fixed-point check binds to CANDIDATE not Stage1[k] (briansrls inline BLOCKING) briansrls flagged a load-bearing THESIS-facet-2 / T-15 violation at line 531: PromotionWitness composed a k+1 bootstrap-roundtrip check with a fixed-point check over Stage1[k] (the OLD stage). That would let the promotion gate replace stage0 without ever proving the CANDIDATE is a self-emitting fixed point — Stage1[k]'s stability was already proven at the prior k-1 → k promotion, so re-checking it proves nothing about the new candidate. A non-self-emitting candidate could pass the gate and become Stage0[k+1]. THESIS facet 2 (compiler self-emits) would no longer hold by construction. FIX (3 sites): 1. Line 531 (bootstrap substrate table — the inline-flagged line): PromotionWitness composes (a) candidate-bootstrap-roundtrip — Stage0Candidate[k+1] produces Stage1Candidate[k+1] (b) candidate-fixed-point — Stage1Candidate[k+1] compiles to itself Both sub-checks now explicitly bound to the CANDIDATE at k+1, with an explicit warning that the fixed-point check is NOT over Stage1[k] and why (otherwise the gate could promote a non-self- emitting compiler). 2. Line 511 (witness taxonomy table): PromotionWitness 'What it asserts' clause now says "This CANDIDATE (Stage0Candidate[k+1] + Stage1Candidate[k+1]) is promotion-ready: the candidate Stage1 is a fixed-point AND the candidate Stage0 bootstrap-roundtrips to the candidate Stage1" — matches (1). 3. Line 419 (epoch loop diagram): The in-epoch stability invariant 'verify(Stage1[k] == Stage1'[k])' was incorrectly bound to PromotionWitness[k].fixed_point_sub_check. It's not — PromotionWitness[k] was bound at the prior k-1 → k promotion (over the candidate that BECAME Stage1[k]). The in-epoch verify is a steady-state stability re-confirmation, not a PromotionWitness production. Updated the diagram to: - Explicitly call the in-epoch line 'in-epoch stability invariant' with a NOTE explaining it's NOT a promotion-witness check. - Update the 'Upgrade k → k+1' verify block to show both sub-checks binding to PromotionWitness[k+1] over the CANDIDATE: Stage0Candidate[k+1] can produce Stage1Candidate[k+1] ──> PromotionWitness[k+1].candidate_bootstrap_roundtrip_sub_check Stage1Candidate[k+1] is a fixed-point (self-emits) ──> PromotionWitness[k+1].candidate_fixed_point_sub_check - Add explicit closing note: 'gate requires both sub-checks pass — non-self-emitting candidate CANNOT be promoted; THESIS facet 2 holds by construction.' The previous wording was a paste-up artifact from the BootstrapWitness + FixedPointWitness collapse: the old FixedPointWitness was steady- state stability, and when we composed both into PromotionWitness I didn't re-bind the fixed-point check to the candidate. briansrls caught it correctly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…3442) * WIP: Modeling * v4 TASKS: schedule HostModel / ModelCore / Protocols substrate (Ratified Q1 + P4) PR #3437 (commit deda6f2) ratified three substrate concepts in `docs/design-v4-compiler-homomorphism.md` that had no TASKS.md home: - **Ratified Q1 (2026-05-20)** — `HostModel` is a distinct peer of `LanguageModel`, both extending a shared `ModelCore`. Files needed: `std/model_core.dag` + `std/host.dag` (neither exists on main). - **P4 (2026-05-20)** — Glue derivation is a composed homomorphism; `extdeps/protocols/` is named verbatim as "Currently missing" substrate (REST / GraphQL / gRPC). Adds three rows: - **T-33** `std/model_core.dag` — shared substrate factoring [needs T-1, T-2, T-3] - **T-34** `std/host.dag` — HostModel peer of LanguageModel [needs T-33] - **T-4.15** `extdeps/protocols/{rest,graphql,grpc}.dag` — transport substrate, P4 [needs T-3, T-26, T-4]; out-of-scope for initial single-target compiler, in-scope so glue derivation isn't foreclosed Plus the parallel-fill execution-graph block at top of file is updated to list the three new rows. No new doc, no anemia-audit work, no Wave-1 LanguageModel fleshout — T-30 owns the structural anemia gate, T-4 owns the fact-bundle rework, and `docs/audit/coproduct-anemia-inventory.md` is the existing one-shot census. The catalogue-doc shape the original brief proposed collided with the operator's standing ledger principle (CLAUDE.md, 2026-05-19); this PR is the narrower form the operator ratified instead — three TASKS.md rows, zero new docs. T-4's `[needs …]` is intentionally NOT edited here. Once `model_core.dag` lands, the T-4 fact-bundle authoring contract should be re-expressed in terms of "LanguageModel extends ModelCore" — that reconcile is its own commit train, not bundled with the substrate landing. The Q1 ratification established the SHAPE; landing the carrier file and re-routing T-4's authoring are two separable steps. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: wire T-33/T-34 into T-4/T-22 graph edges (codex review #3442) Addresses two of the three codex findings on PR #3442 (BLOCKING): - **T-33 → T-4 edge.** Reviewer correctly observed that T-33's body claims "consumed by T-4 (LanguageModel)" but T-4's `[needs …]` contract omitted T-33 — so LanguageModel could be scheduled before its shared substrate facts exist. Fix: add T-33 to T-4's `[needs T-3, P1-KEYSTONE, T-29, T-30, T-25-core, T-33]` in both the side-branch graph block (top of file) and T-4's task-definition body. Side-branch graph + feeders block updated to four → five feeders. T-33's own task body unchanged. - **T-34 → T-22 edge.** Same shape — T-34's body claims "Consumer: T-22 eval + MVP-B route" but T-22 still needed only T-9. Fix: T-22's parallel-fill execution-graph entry now `[needs T-9, T-34]`, with a one-line note pointing at the Ratified Q1 origin. NOT done in this commit (deliberate): - **T-22's task-definition body signature `eval: (InferredTree, Inputs)`** is not updated to include the HostModel parameter. Adding the graph edge records the dependency; restructuring eval's signature is a substantive modeling change and stays a separate commit train. - **T-4's body text on "fact-bundle authoring contract"** is not re-expressed in terms of "LanguageModel extends ModelCore". Same reasoning — graph edge ≠ authoring-contract reconcile. The third codex finding (`docs/design-v4-compiler-homomorphism.md` absent at PR head) is a false positive — the bot reviewed `fecd3bd0` (the WIP snapshot) and reported the file as missing, but the file landed in `deda6f210` (PR #3437) on main 2026-05-20 03:23 and is present at every commit on this branch. Blob hash `6afcb0914dbf3884b687ab7f3696b00dbacf1fa2`, 1333 lines, verified at PR head + origin/main + origin PR branch. Reply on that thread, no fix commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: reconcile stale T-33 prose with the T-4 [needs] edit (codex review #3442) Addresses codex review verdict REQUEST_CHANGES (dashboard review id 15297, sha 2b928e8). The earlier graph-edge fix 6d7e152 added T-33 to T-4's [needs] but left T-33's body paragraph claiming "No silent change to T-4's [needs …] list as part of this PR" — true at 2b928e8, FALSE at 6d7e152. P2 single-authority problem inverted: prose now denied what [needs] actually did. Fix: rewrite T-33's "Dependencies" paragraph to acknowledge the edit explicitly. New framing names what this PR DOES touch (T-4's [needs] schedule edge — added) vs what it does NOT touch (T-4's fact-bundle *authoring contract* body prose — separate commit train, after T-33 lands). Single-authority for the dependency fact lives in T-4's `[needs …]` line, not in T-33's prose. T-34's body "Consumer: T-22" claim is consistent with T-22's [needs T-9, T-34] after 6d7e152 — no edit needed there. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: drop T-4 from T-4.15 [needs]; transport is language-orthogonal (codex review #3442) Addresses codex review id 15305 (REQUEST_CHANGES on 7ecdf4e): the T-4.15 dependency rationale wrongly tied the transport substrate to T-4 language carriers, with prose claiming "protocols often parameterize over the host language's type system." That collapsed the transport model into language-specific concerns — the opposite of P4's "shared transport model" framing in `docs/design-v4-compiler-homomorphism.md` (§ "P4 — Glue derivation is composed homomorphism, orthogonal to the compiler"). Fix: - T-4.15 [needs T-3, T-26] (T-4 dropped) in both the execution-graph block and the task-def body. - New rationale paragraph names the language-orthogonality explicitly: each transport declares its own wire-format type system (REST: HTTP bodies + headers; gRPC: protobuf primitives; GraphQL: GraphQL type system). LanguageModel bindings happen at T-16's omni-stack composition (LanguageModel ∘ TransportModel ∘ LanguageModel via the coercion fold — P4's "applied twice through a shared transport model"), NOT on the transport substrate itself. T-33 / T-34 unchanged — codex's verdict confirmed they line up with the ratified Q1 shape. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: relocate T-4.15 to "Close-the-loop + late substrate"; gate the deferral (openai-pro review #3442) Addresses openai-pro review verdict REQUEST_CHANGES (dashboard review id 15302, ran on sha 7ecdf4e at 2026-05-20T08:44:22Z). The finding: single-authority violation on T-4.15's schedule fact. The parallel-fill block put T-4.15 under "schedule the instant deps clear" with `[needs T-3, T-26]`, but the task-def body says "file authoring waits until omni-stack glue work activates (T-16 timeline)" — two contradictory schedule authorities, so a worker following the graph would dispatch when T-3/T-26 land while a worker following the body would wait. Fix: - Move T-4.15 OUT of the "Substrate / extdeps fan-out" sub-block of the "instant parallel fill" section. - Move T-4.15 INTO "Close-the-loop + late substrate" alongside T-26 (its closest semantic neighbor — both are boundary substrate awaiting downstream activation). - Add an explicit deferral gate: "scheduled-but-deferred — file authoring activates with omni-stack glue work per P4." Single authority for the activation gate now lives on this schedule line + the task-def body's "Out of scope for the initial single-target compiler" section, both saying the same thing. - Leave a one-line pointer in the old position so a reader scanning the parallel-fill block still finds T-4.15 quickly. No change to T-33, T-34, or any other row. CI is passing on the prior HEAD (7ecdf4e); this push will re-run CI on the new HEAD. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: remove T-33 duplicate from "Close-the-loop + late substrate" (openai-pro review #3442) Addresses openai-pro review verdict REQUEST_CHANGES (dashboard review id 15306, ran on sha 1713538 at 2026-05-20T08:58:33Z). The finding: T-33 was placed in BOTH the side-branch feeders block (correct — as a watch-item T-4 prerequisite that goes critical if it slips) AND the "Close-the-loop + late substrate" block (wrong — implying slack/late). Contradictory priority signals — a worker reading the late-substrate bucket would schedule T-33 late, opposite to the side-branch's hard-prerequisite framing. Fix: remove T-33 from the "Close-the-loop + late substrate" block. The side-branch feeders block at the top of the file remains the single authoritative placement, carrying the correct watch-item semantics. Leave a one-line pointer in the late-substrate block so a reader scanning that section still finds T-33 quickly. T-34 and T-4.15 stay in "Close-the-loop + late substrate": - T-34 feeds T-22 (eval), which is in "Interpreter + lens dimensions", not on the critical path — no contradiction. - T-4.15 is explicitly scheduled-but-deferred (activates with omni-stack glue) — the bucket signal matches the deferral gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 TASKS: clarify T-4.15 is NOT a current T-16 dependency (codex review #3442) Addresses fresh codex BLOCKING finding on PR #3442 (comment 3272726241, 2026-05-20T09:24:41Z, on sha 186a0c3, line 1331): "T-4.15 says T-16's glue derivation composes through TransportModel, but T-16's authoritative needs line still omits T-4.15, so the new substrate fact can be scheduled after its consumer (facts-flow-forward / P2)." Valid finding — T-4.15's body claimed T-16 consumes TransportModel, but T-16's `[needs T-4, T-4.5, T-4.6, T-4.7, T-4.8, T-10, T-11]` is OpenAPI-based (via T-4.6 openapi.dag + T-4.8 coordination.dag's WireContract) and doesn't include T-4.15. The protocols substrate is for a FUTURE omni-stack expansion beyond T-16's current scope, not a current T-16 dependency. Fix: T-4.15 body softened in three places to distinguish T-16's current OpenAPI scope from the future expansion that activates T-4.15: 1. Opening paragraph: "the eventual T-16 omni-stack glue derivation" → "a future omni-stack expansion (beyond T-16's current OpenAPI-based wire-contract scope)". Added explicit note: "T-16's authoritative `[needs]` does NOT include T-4.15." 2. Dependencies paragraph: "T-16's omni-stack glue derivation composes ..." → "a future-expanded omni-stack glue derivation (beyond T-16's current OpenAPI scope; not part of T-16's current `[needs]`) composes ..." 3. Out-of-scope paragraph: "(T-16 timeline)" → "*beyond T-16's current OpenAPI scope* (a future expansion; T-16's `[needs]` does NOT list T-4.15 today)" Single-authority restored: T-16's `[needs]` is the authoritative source for what T-16 currently consumes; T-4.15's body now correctly says it is NOT in that set today. T-16's `[needs]` is intentionally not edited — the dependency edge doesn't exist in T-16's current scope, so adding T-4.15 would falsely assert a consumer relationship. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: Modeling * v4 TASKS: align T-22 with Q1 (eval reads HostModel) + add T-33 [needs] (codex review #3442) Addresses two real codex BLOCKINGs from the latest run on 56256ab (comments 3273505059, 3273505180): 1. **T-22 line 919 — concept-unification bullet still claimed eval reads `extdeps/languages/*.dag`.** That framing pre-dates the Ratified Q1 split: post-Q1, eval reads HostModel (T-34) for primitive interpretation, execution semantics, and host value representation; LanguageModel is for ingest grammar + emit serialization. Sharing only ModelCore (T-33) for primitives / algebra / laws / effects / partiality. Bullet rewritten to name that split and explicitly mark the prior framing as superseded. Resolves the P2 single-authority concern: T-22's new HostModel signature is no longer paired with a stale "eval reads LanguageModel" claim. 2. **T-33 line 1212 — body had no canonical `[needs]` line.** The side-branch feeders block at line 110 mentions "(needs only T-1, T-2, T-3)" in prose, but Practice 5 / single-authority asks for the `[needs …]` line to live on the task-def body too — as T-26, T-29, T-30, T-34, and T-4.15 all do. Added explicit `**Dependencies — `[needs T-1, T-2, T-3]`.**` paragraph at the top of T-33's body, naming the upstream facts (T-3 numeric stack, T-2 algebra, T-1 Node root) + framing T-33's "low-dependency but hard T-4 prerequisite" position from the side-branch graph. T-34 and T-4.15 bodies already carry their `[needs]` lines — no additional edits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
What this PR is
A draft architecture document for the v4 compiler — written to be readable cold, not just by project insiders. It captures what the compiler should be, mechanically, if we take THESIS's "The derived homomorphism" claim literally.
The doc is at
docs/design-v4-compiler-homomorphism.md. It now includes:gunbcis, what the.dagsubstrate is, and what "homomorphism" means in this context — for newcomers..dagsource going through the pipeline (add(x, y) = x + y→ both Rust source AND eval-to-Value).fold_node,coercion fold,LanguageModel,InferredTree, Practice 8/9/10, T-8/T-9/T-10/T-22, D2 reversal, fail-closed.TL;DR for reviewers familiar with the project
The v4 compiler is one structural primitive (
fold_node) plus four substrate operations (diagnostic carrier, grammar-as-bidirectional-data,traverse, the coercion fold per TASKS.md T-9). Every "pass" is an algebra plugged intofold_node. The compiler knows no specific language — Rust, Python, etc. areLanguageModeldata passed in.The external surface:
Two parameters; one fail-closed Outcome. Eval is structurally translate-to-host. The lens question is explicitly open (see Q0).
Status of the two BLOCKING review findings
Why this exists
Implementation briefs for T-9 / T-10 / T-22 should not be drafted until the architecture is settled. v2 cemented
emit_rustbecause nobody wrote down what emit should be in advance. We do not want to repeat that in v4.How to engage
Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com