Repository navigation
docs(design): read/edit pipeline — node-centric agent surface - #3364
Conversation
Adds six proposed Layer-1 lenses derived from the 2026-05-18 review ingest against `main@e7b8a8d` (corroborated against worktree HEAD). Each section follows the existing L1.x format (signature / decidability / verdict / escape / kills) and includes concrete code-level match cases + clean-shape examples, so the structural signature is reviewable without chasing repo paths. - L1.7 Off-substrate-fact — prose-asserted facts (F3 lattice, F4 width, F11 opacity). Generalizes the standing "machine-readable inhabitance" ruling. - L1.8 Wrong-home — orphan operations (F5 `nat_compare` in float.dag). Mechanizes MODELING M9. - L1.9 Vacuous-arm — exhaustive-but-empty match (F1 `ComputationNode { behavior: _ } => true`). - L1.10 String-escape-hatch — typed-model bypass via String (F6 `ShellCommand { command: String }` vs typed `process.Command`). Generalizes L1.6. - L1.11 Plausible-fallback — fabricated-sibling fallthrough (F10 `DELETE None => CreateEffect`). - L1.12 Parallel-authority — unmarked duplicate concept homes (F9 `dsl/std` vs `src/v4/std`; D2-resolver provisional + planned-absent). Each carries `Status: proposed` in the section header. Slipped-by ledger (§8) gains corresponding rows pinned to current main file locations so the evidence is grep-anchored per §3 methodology. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…y gap cursor/composer-2 review noted that the F9 "Concrete match" block implied both `dsl/std/types.dag` and `src/v4/std/logic.dag` were bare, when both files actually carry annotations above their `type Bool` line (legacy-scanner anchor prose in dsl/std/types.dag:163-172; 🟢 coproduct-dissolution classification tag at src/v4/std/logic.dag:13). The lens's case is sharper, not weaker, once the existing tags are visible: they classify the finding shape (dissolution status, scanner anchor) but neither *designates authority* between the two parallel declarations. L1.12 specifically requires a designator that picks a canonical winner, which is the gap classification tags don't fill. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Addresses three BLOCKING findings on the L1.7–L1.12 proposal:
L1.7 — width discharge must be recursive. The previous signature/clean
shape allowed a `Word64 { bytes: List<Byte> where len(_) == 8 }` that
bottomed out at an unconstrained `Byte`, so an arbitrary-bit-count
`Byte` still inhabited a "well-formed" `Word64`. Signature now requires
a recursively-discharged refinement chain down to a fixed-cardinality
leaf or primitive bit; clean-shape example shows the full
Word64 → Byte → Bit chain and structurally distinct Float32/Float64
exponent/significand widths instead of a shared `FloatBody`.
L1.8 — primary-concept selector replaces the argument-files heuristic.
Previous signature ("every argument's type lives in file X") missed
witness-target homing (a `meet` field of `Lattice<T>` belongs with T,
not with whichever file declared its argument types). New four-rule
structural cascade in priority order:
(1) declared witness target → algebra's type parameter is the home;
(2) same-type closure (`fn(T,T)→T` etc.) → T is the home;
(3) upstream argument+return convergence on file X → X is the home;
(4) no single owner → cross-cutting, lens does not fire.
L1.12 — escape valve must be structural, not prose. The previous
"// Authority: canonical | historical" comment markers were prose-
as-authority — exactly the shape L1.7 exists to kill. The lens is now
self-consistent: only structural shapes discharge it — alias/import
identity from historical to canonical, a `data ... :
HistoricalDeclaration` row in a retirement ledger read as data, or
deletion+migration in the same change. Comment markers explicitly do
not satisfy the escape, by construction.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…cts only Addresses three BLOCKING findings from codex review on cfbc247: L1.9 — replace function-name suffix vocabulary with intra-match asymmetry. The previous signature gated on `*_well_formed` / `*_valid` suffixes — naming as a structural fact, which violates P1 ("heuristics are never structurally necessary"). New signature is purely structural: a single match where ≥1 arm has a trivial-literal RHS AND ≥1 sibling arm does non-trivial structural work. The discipline-role is inferred from the fact that the author already wrote real work for some variants, which makes the trivial siblings a vacuum. The F1 node_locally_well_formed case still fires (TypeNode arm calls edges_conform, ComputationNode arm returns true). L1.10 — replace hardcoded `command`→Command / `path`→Path / `url`→Url field-name table with a substrate-declared canonical-carrier registry. A typed carrier declares `data X: CanonicalCarrier<X> = { supersedes_string: { in_role: <role-tag> } }`; the lens reads the registry. Adding a new typed carrier is now a `data` row in `extdeps/`, not an edit to the lens definition. The lens carries no domain names. L1.12 — split planned-absent-import out of the duplicate-authority lens. They are different failure shapes: duplicate `type T` in two files is a duplicate-authority finding; a dangling import path is an unresolved-reference / fail-closed P3 finding. Collapsing them under one verdict reports the wrong root cause. L1.12 narrows to duplicate-declaration; planned-absent moves to an L0.8-extended row in the slipped-by ledger. The D2-resolver concrete-match block is retitled as a cross-reference note explaining why it does *not* collapse into L1.12. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
codex review on 3fb3e4d raised two valid findings: L1.10 — the role-tag refinement created an opt-in opportunity for authors to bypass the typed-carrier rule by omitting the tag. The escape "no role-tag refinement, passes" was convention-level enforcement, not API-level. New signature drops the role-tag mechanism entirely. The CanonicalCarrier registry declares a `supersedes_string_at_field_named` set (substrate data); the lens fires on any String field whose name appears in any in-scope registry entry, unconditionally. The author cannot bypass by omitting an annotation because there is no annotation — the trigger is the field name they chose plus the registry-declared coverage. Legitimate raw-string exemptions move to structural Exemption rows in the same registry, read as data. L1.12 — the prior signature said "type T = ..." literally, which only matches the alias/sum form. The slipped-by ledger row claims coverage of duplicate machine-word homes, but `type Word64 { bytes: List<Byte> }` is record form and would have escaped the literal signature. Broadened to "any `type T` declaration form" — sum/alias, record, unit, generic — with explicit enumeration of the covered forms so the signature unambiguously matches the cases in the section's own examples and ledger. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The original L1.1–L1.6 sections describe each lens by signature /
decidability / verdict / escape / kills, but did not show what the
matching code or the discharging code actually look like. Adds the
same "Concrete match" + "Clean shape" example blocks the proposed
L1.7–L1.12 sections use, so each lens is concretely readable without
chasing the referenced PRs.
- L1.1: basic discriminant shape (`nat_is_zero`) + the laundered
constant-algebra fold (`free_monoid_is_empty`-via-fold).
- L1.2: (a) struct-of-functions (`ListMap<A,B>` wrapper) and (b) N
near-identical single-field structs (`{ spelling: String }` ×N).
- L1.3: declared-but-never-inhabited type (`ParseError` with no
constructor, no `data`, no alias, no field).
- L1.4: `Outcome<T>` clone (`NormalizeChildrenResult`), with the
three-variant `Cached | Produced | Rejected` shape as the escape.
- L1.5: clean recursion mirroring data shape (`ci_member` over List)
and the short-circuit `match acc { Rejected => propagate; Ok =>
continue }` ladder (resolve/normalize walkers).
- L1.6: type-construction template tables (`list_template: "Vec<{0}>"`)
vs. structural target-type modeling.
No signature, verdict, or escape semantics changed; this commit only
adds illustrative code blocks.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Implements the consolidation feedback as a middle path: tightens the
conceptual scaffolding without dismantling the lens catalog.
- §1: introduces A0 ("every semantic fact must have exactly one
structural witness") as the umbrella invariant, with A1 retained
underneath as the operation-specific specialization. Explicitly
framed as operationalizing modeling-discipline.md Practice 10, not
as a parallel rulebook, to avoid the L1.12-class parallel-authority
hazard of duplicating Practice 10's principles here.
- §5.0 (new): adds the three-levels framing (Invariant / Theme / Lens),
the lens → theme(s) catalog (derive / witness / canonical-home /
fail-closed), and the explicit disclaimer "themes are explanatory
tags only — they do not define CI gates, test-corpus boundaries, or
implementation passes; the mechanically enforced unit remains the
L1.x lens signature." Per the §3 methodology, each lens's signature
must be the smallest structural pattern that catches its finding's
class with zero false positives, so theme-sharing alone does not
collapse machinery.
- L1.6 → L1.10 merge: the only mechanical merge in this rev, because
the prior doc already stated that L1.10 generalizes L1.6. L1.10 is
renamed "Textual-bypass lens" with two sub-signatures:
L1.10.a TemplateHole — registry-free, catches `{0}`/`{1}`
positional-placeholder string
literals used as emitters
L1.10.b CanonicalCarrier — substrate-declared registry, catches
String fields whose name appears in
a CanonicalCarrier coverage set
L1.6 section becomes a one-paragraph pointer to L1.10.a, preserving
anchor compatibility. The slipped-by ledger's F6 row is repointed to
L1.10.b and a new F8 row is added for L1.10.a.
L1.2/L1.3/L1.4, L1.8/L1.12, and L1.9/L1.11 are intentionally not
merged — their detection machines are mechanically distinct (different
signatures, decidability arguments, escape valves) and the operator
TDD-pairs directive requires distinct test corpora per lens. They
share themes in the §5.0 catalog without sharing implementation.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Five sharpening edits from operator review of the A0/themes pass:
1. A0 rephrased: "exactly one structural witness" → "exactly one
canonical structural witness *path*". Alias / re-export edges,
retirement-ledger rows, and derived operations reading the same
witness all point at one authority; they are the path, not a
multiplicity that violates A0.
2. §2 "one substrate gap" claim updated. The original sentence was
true for the L1.1/L1.5 seed findings but too narrow for A0's
broader territory. Now distinguishes the seed gap (no derived
discriminant/catamorphism → workers hand-roll them) from the
general gap (missing witness table / authority map / refinement
edge / diagnostic carrier → workers encode locally in prose /
names / strings / duplicate homes / plausible defaults).
3. L1.10 explicitly renamed "Textual-bypass lens family" with an
"Exception to §5.0" note: L1.10.a TemplateHole and L1.10.b
CanonicalCarrier are the mechanical units, sharing a finding
family and reporting label but keeping separate signatures,
decidability arguments, escapes, and test corpora. Resolves the
tension between §5.0 ("the mechanically enforced unit is the L1.x
signature") and L1.10's two-detector structure.
4. L1.6 stub retitled "Deprecated alias — see L1.10.a `TemplateHole`"
so old test names and slipped-by references remain traceable.
5. §8 trailing prose fixed: "all four are burn-down substrate PRs"
was true when the ledger had four rows; now it has the four seed
rows plus the ingest extension. Reframed as "Pattern from the seed
PR rows" with an explicit note that the ingest rows extend the
ledger to A0's broader territory.
6. A0/A1 ratification sentence made authority-chain explicit: "Once
ratified into Practice 10, A0/A1 become citable hard rules; this
doc remains the enforcement mechanism." Avoids the rulebook-ish
phrasing that suggested A0/A1 were independently citable.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a new §10 (renumbering audit to §11) answering the "how does this run / is it parallelizable / how much work" questions operationally. The core framing: there is no "lens framework" separate from the compiler pipeline. Lenses are .dag stages that declare consumes: edges against the existing parse/resolve/infer producers, and the compiler's stage-ordering schedules them automatically. - §10.1: shared-indices taxonomy — maps each shared structural fact (AST, symbol resolution, variant lists, inhabitance edges, witness registries, refinement clauses, import graph, fail-closed return- type carriers) to the existing pipeline stage that produces it and the lenses that consume it. Most of what lenses need is already computed; lenses just query. - §10.2: three small derived stages cover what the existing pipeline doesn't yet expose — match_arm_shape (reusable by L1.1, L1.9, L1.11, L0.7, L0.13), closed_vocab_scan (L1.7), concept_home (L1.8). Each is a single deterministic fold; reusable across multiple lenses by design. - §10.3: a lens is just another .dag stage with declared dependencies. Adding a lens = land a stage; the existing compiler stage-ordering handles scheduling. No new framework. - §10.4: per-file and per-lens parallelism fall out of the dependency graph automatically; affected_set integration scales CI cost with PR size, not corpus size. - §10.5: summary of operational properties — one dependency model across pipeline + lenses, lens addition = stage land, index addition = small derivation stage shared by all lenses that need it, self-application clean (the compiler enforces the discipline it follows). This is the L1.12-class self-consistency check: a separate "lens framework" with its own dependency model would itself be parallel authority, which the lens suite exists to kill. The dependency-model section makes explicit that the lens framework reuses the pipeline's existing modeling — one dependency system for everything. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…cal L1.x keys Bundles three changes operator-routed via witty-cat-59 as the #3313 stabilization trigger: 1. **L1.11 plausible-fallback** — drop the "return type is not Outcome<_>" carve-out that was a false negative on `fn(...) -> Outcome<T>; None => Produced { value: ... }`. Replaces with a structural FailClosedDiagnostic registry declaring Outcome::Rejected as the registered fail-closed constructor. The lens fires on RHS Ctors that are not registered as fail-closed, covering both the F10 bare-return case AND the Outcome-wrapped fabricated-success case the prior signature missed. or_default-style total-by-design helpers escape via a structural PlausibleFallbackExemption row, same shape as L1.8 WrongHomeExemption and L1.9 VacuousArmExemption — no comment anchors. 2. **L1.12 parallel-authority** — reframe so lexical-name collision is the *trigger* (not the conclusion), with four resolution paths the lens checks against the substrate: (1) same-concept-with-alias (CanonicalConcept row + alias edge) → passes (2) same-concept-without-alias (CanonicalConcept row but no alias) → fires (the original duplicate-authority case) (3) distinct-concepts (ConceptDisambiguation row marks them as legitimately different) → passes (4) silence (no row in either registry) → **fires as unresolved-duplicate** The prior formulation only fired on (2) and missed (4) — the F9 motivating case where Bool was declared in two files with no CanonicalConcept row anywhere. The substrate must take a position on every cross-file lexical collision; silence fails closed. 3. **§5.1 Canonical L1.x acceptance-key names** — new subsection enumerating the stable canonical key names downstream consumers (e.g. coverage.dag's dissolution_l1_* rows) must use. The lens suite is the single authority; downstream key sets are projections. Includes explicit migration notes: - `dissolution_l1_6_emit_template` → retired, no L1.6 key - `dissolution_l1_10_string_escape_hatch` → split into `dissolution_l1_10_a_template_hole` AND `dissolution_l1_10_b_canonical_carrier` This is the #3313-stabilization step in #3322's closeout register (item 7). On land: - warm-koi-304's #3318 (held-at-track-not-finalize) can rebase against the stable §5.1 enumeration - batch-(d) remains held until A1 invariant placement PR lands too Routed via witty-cat-59 (program-coordination); follow-up PR owned by sunny-wolf-435 as #3313 author per #3322 closeout-register row 7. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…silence)" cursor/composer-2 review noted editorial inconsistency: the text said "exactly one of three resolutions" but the list enumerated 1-4 with silence as case (4). Corrected to "one of four outcomes — three passing resolutions plus a fail-closed silence case" so the prose matches the structural enumeration that follows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reviewer (briansrls 2026-05-18T23:26Z) flagged that the prior wording said "three passing resolutions" but the enumerated 1-4 list had only TWO passing (alias, ConceptDisambiguation) and TWO firing (same-concept-without-alias, silence). The HistoricalDeclaration retirement-ledger and deletion/migration paths from the Escape section were "outside the stated decision table" — a P2 decidable-single- authority violation. Fix: restructure the enumeration to cover ALL mechanically-distinct outcomes inline, so the decision table is closed: (1) Same-concept-with-alias → passes (2) Same-concept-with-retirement-record → passes (new: was in Escape) (3) Distinct concepts (ConceptDisambiguation) → passes (4) Same-concept-without-alias-or-retirement → fires (original duplicate-authority case) (5) Silence → fires (unresolved-duplicate) Three passing + two firing = the arithmetic now matches. Deletion / migration is explicitly noted as "not a fifth resolution" — it removes the trigger condition entirely (no lexical collision), so the lens never engages, which is mechanically distinct from a resolution. The Escape section is collapsed to a pointer at outcomes (1)/(2)/(3) to avoid duplicating the decision-table content. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes the residual gap on the wrap BLOCKING review: outcome (2) "Same-concept-with-retirement-record" consults a HistoricalDeclaration registry row, but the prior Decidable bullet listed only CanonicalConcept + structural-alias + ConceptDisambiguation. Now every registry the 5-outcome decision table consults is named in the decidability statement explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
cursor/composer-2 review caught a contradictory-guidance bug: the new
L1.11 bullets explicitly include the Outcome-wrapped case
(fn(...) -> Outcome<T>; None => Produced { value: ... }) as firing,
but the Verdict still said "lift the return type to Outcome<T> and
return Rejected" — which doesn't address the case that's already
Outcome-wrapped.
Split the fix into two case-specific guidances:
- Bare-return case: lift return type to Outcome<T>, return Rejected.
- Outcome-wrapped case: replace Produced ctor with Rejected
{ diagnostic: DerivationUnknown } on the missing-info arm.
Same underlying fix shape (escalate missing info through the
registered fail-closed-diagnostic variant) — just two distinct
starting points depending on which form of fabricated-success the
lens caught.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… OR CanonicalConcept co-membership) codex review (REQUEST_CHANGES) caught a real semantic weakening in the prior "lexical collision is the trigger" rewrite: two parallel homes for ONE concept with DIFFERENT names would slip past the lens entirely, contradicting P2 / Practice 5's concept-level single-authority demand. Fix: restore concept-level detection by adding Trigger B (concept- graph) alongside the existing Trigger A (lexical). The lens fires on parallel authority detectable in EITHER way: - **Trigger A (lexical):** cross-file `type T` declarations sharing a simple name. (Existing; catches the F9 motivating case.) - **Trigger B (concept-graph):** two `type T1` / `type T2` declarations in different files that are co-members of a `CanonicalConcept` row, regardless of whether their lexical names match. (NEW; catches the same-concept-different-name case the prior rewrite missed.) Either trigger enters the same 5-outcome resolution table. Per-outcome under Trigger B: - (1) alias / (2) retirement-record / (4) no-resolution apply cleanly to both triggers - (3) ConceptDisambiguation under Trigger B would CONTRADICT the CanonicalConcept co-membership row — registry-inconsistency, caught by L0-class checks, not L1.12 - (5) silence is NOT reachable under Trigger B (the trigger IS a registry row's presence); only reachable under Trigger A Also added an explicit Decidability Boundary note: the lens cannot catch the case where two homes use different names AND no CanonicalConcept row registers them as the same concept. That's a P2 violation but mechanically undetectable from parsed substrate alone — closing it requires either operator judgment or a future structural-similarity-fold primitive. Per §3 methodology, lens signatures catch their class with zero false positives; Trigger B's CanonicalConcept-driven gate is the structural surface decidable today. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… spec) Frames the substrate's read/edit surface for arbitrary code at the Node level — not the file level. Files are a delivery / persistence mechanism modeled via extdeps/file_system.dag; the language doesn't couple to them. Reads target Nodes (and scopes within Nodes); writes are structural Edits to Nodes; Node-to-File binding is its own concern, modeled alongside Node, not inside it. Operator-stated motivation (2026-05-19): the mechanical part of shifting bits isn't the hard part — the INTERFACE is. This doc captures the design intent + worked examples + open interface questions, especially for LLM/agent consumers. Doc structure: - §0-1: framing — why node-centric, not file-centric (3 reasons: files decoupled from concepts; edits should be structural; agent reasoning is at concept level) - §2: read interface — apply_lens(lens, scope, mode) per QRY-1 ratification (2026-05-15); no separate query subsystem; lens catalog + composition - §3: write interface — Path/Edit/Diff per #3162 ratification; apply_diff fold semantics (all-or-nothing fail-closed) - §4: read → edit pipeline — six-step closed loop (Read → Diagnose → Propose → Gate → Apply → Re-emit). Files only re-enter at Re-emit; they're a downstream effect of substrate state. - §5: three worked examples — (A) bare-alias refactor to canonical-B (same shape as #3338); (B) rename a concept across the corpus via CanonicalConcept registry cascade; (C) TestClaim breakage diagnosis + fix - §6: six open interface questions — higher-order Edit combinators, composition under overlap, intent-shaped declarations (generalized Track 2), LLM-targeted diagnostic shape, workflow-as-data for the agent loop, structural provenance traces - §7-8: scope clarifications + status Status: design spec; mechanical primitives exist, T-23 realizes them; the six open interface questions are where the substantive interface design work lives. No implementation prescribed. This is operator-requested framing work, not action work. Each open question becomes its own follow-up doc / PR when picked up. 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:
1dcf5193· Trigger:schedule - Thinking:
225s wall
BLOCKING (3)
Root Cause
docs/design-read-edit-pipeline.mdThe doc conflates low-level filesystem modeling with emit provenance → point at the actual Node/File binding carrier or add that missing carrier/open dependency before relying on node-centric re-emit.docs/design-read-edit-pipeline.mdThe examples use higher-level edit verbs before they are defined over the ratified replacement-only carrier → either express them as replacement-at-path rewrites or mark them as a future combinator layer.docs/design-read-edit-pipeline.mdThe doc collapses selection output into scope input → fold over frontier-selected paths/declarations to build validDeclarationScope/NodeScopevalues, or explicitly design a new scope carrier.
| file can carry multiple concepts. Reading at file granularity | ||
| loses concept structure. | ||
| 2. **Edits should be structural, not textual.** A textual edit at | ||
| "line 42" doesn't compose; a structural Edit at a `Path` composes |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| **The lens catalog** (`src/v4/lens/*.dag`, 12 files): | ||
| - `affected_set` — incremental re-exec frontier | ||
| - `application` — the `apply_lens` surface itself (the meta-lens) | ||
| - `complexity` / `cost` — complexity / cost projection |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| (or that `affected_set(dag, diff)` derives). | ||
|
|
||
| **Mode** = what the lens does: | ||
| - `Introspect` — read-only; produces a structural fact carrier |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Two findings — Finding 1 valid, fix pushed; Finding 2 factually wrong, rebutting on-PR. Finding 1 (L1.12 concept-identity carriers undeclared in substrate) — VALID. Verified: `CanonicalConcept` / `ConceptDisambiguation` / `HistoricalDeclaration` are NOT in any of `src/v4/std/.dag`, `src/v4/lens/.dag`, `src/v4/extdeps/*.dag`. They exist only as design in `docs/design-dissolution-lens.md` (PR #3334, operator manual-merge queue) — design-described, not ratified substrate. Fix in `07d862f91`:
Finding 2 (unlanded thesis retraction used as authority) — FACTUALLY WRONG. The thesis retraction IS landed in THESIS.md. Direct read of `origin/main:THESIS.md`: Line 232:
Line 288 (under facet 4):
So the narrowing I cite in §7.5 ("`workflow/agent_loop.dag` is not the right place; the THESIS narrowing stands") IS in higher-authority THESIS.md with the explicit operator-ratification stamp. Not an unlanded retraction; this is the citable authority. The relay may be looking at a stale THESIS.md or missed the parenthetical retraction note on line 232. No change needed on §7.5. — sent from sunny-wolf-435 |
…g §6.4 Same finding fired again at line 255 of pre-fix sha (§5 Example B "rename a concept across the corpus", which also references CanonicalConcept). The global §6.8 item 8 + §6.4 inline caveat from 07d862f cover the case, but a reader entering at §5 Example B should see the dependency callout immediately — same shape as the §6.4 callout. Both inline caveats point at §6.8 item 8 as the global tracking entry. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Already addressed plus tightened (`07d862f91` then `2c6a3cdb9` for this specific anchor). Relay points at line 255, which is in §5 Example B's intro — same finding class as the codex wrap I addressed, just a second site. Coverage on current HEAD:
P1/P2 compliance restored: the carriers are tracked as missing substrate, not asserted as ratified authority. The substantive design intent (CanonicalConcept as the concept-identity source-of-truth when it lands) is preserved; the honest accounting is that today it's design-only-pending-#3334. — sent from sunny-wolf-435 |
|
This finding is factually wrong on three counts. The §7.5 claim is directly aligned with what THESIS.md explicitly says. Verified by direct read of `origin/main:THESIS.md`: The reviewer claims: "THESIS.md still commits meta-process/dev-process workflows and R3 tracks Workflow-As-Data plus Lens-Self-Application." What THESIS.md actually says: Line 232 (under facets list):
Lines 266-278 (facet 4 — Recursive-flex / self-application):
Lines 279-289 (explicit retraction of Workflow-As-Data):
Counterpoint by point:
The §7.5 framing ("`workflow/agent_loop.dag` is not the right place; the THESIS narrowing stands") is a direct echo of THESIS:288-289's "`workflow/` substrate is correspondingly `{ bootstrap, ci }` only." Not an unlanded retraction; not a contradiction with higher authority — the higher authority is the retraction. No change needed. — sent from sunny-wolf-435 |
…LOC rename openai-pro REQUEST_CHANGES on f3d146b raised two valid design-level findings; both addressed. **Finding 1 — candidate authority not typed into gate surface.** The candidate-state pattern from earlier was correct in intent, but the worked examples called `apply_lens(_, ref, Enforce)` with a bare ref — leaving the candidate-vs-pre-edit context to a prose comment ("evaluated in candidate_dag context"). A worker following the pseudo-code could accidentally enforce against the wrong root. Fix: introduce `scope_in(root: Node, ref: NodeRef) -> SectionRef` as the helper that **explicitly binds a frontier ref to a dag root**. Updated §4 pipeline + §5 Example A + §6.3 catamorphism + §6.6 CLI + §6.7b mechanical refactor — every gate call now reads `apply_lens(_, scope_in(candidate_dag, ref), Enforce)`. The candidate root is structurally visible in every call; can't be lost via comment-level convention. **Finding 2 — "affected LOC" reintroduces file/line authority before Node→File binding exists.** §6.7b promised "affected LOC" structurally — but §1 explicitly says file/line is emergent-not-substrate. Promising LOC enumeration before the Node→File binding registry (§6.8 item 6) is built contradicts the node-centric framing. Fix: rename §6.7b "Affected-LOC enumeration" → "Affected-structural- paths enumeration"; the inline preview computes structural Paths, not file:line. Added a callout explicitly tying the LOC translation to the Node→File binding registry (§6.8 item 6) — until that registry lands, the substrate-native answer is in terms of Paths. LOC is the downstream projection of "affected sites" via emit's mapping; the substrate-native fact is "affected structural sites." Also updated the "guarantee is structural" close-out: "LOC count is irrelevant" → "Site count is irrelevant." Keeps the doc consistent that the substrate-native unit is the Path/site, not LOC. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Both findings valid; pushed `787ba1bb3`. Finding 1 (candidate authority not in typed gate surface) — fixed. Introduced `scope_in(root: Node, ref: NodeRef) -> SectionRef` helper to make the candidate-vs-pre-edit root structurally explicit in every gate call. §4 pipeline + §5 Example A + §6.3 catamorphism + §6.6 CLI + §6.7b mechanical refactor all updated. Every gate call now reads: ``` — the candidate root is visible in the call signature, not a prose comment. A worker can't accidentally drop the candidate authority. Added explicit prose in §4: "`scope_in` makes the candidate-vs-pre-edit context structurally visible in every gate call — a worker can't accidentally lose the candidate authority by calling `apply_lens(_, ref, Enforce)` with an ambiguous root." Finding 2 (affected LOC reintroduces file/line authority before Node→File binding) — fixed. You're right: §6.7b promised "affected LOC" structurally, but §1 explicitly says file/line is emergent-not-substrate. Renaming preserves the node-centric framing:
Plus an explicit callout tying the LOC translation to §6.8 item 6 (Node→File binding registry): "Until that registry lands, the substrate-native answer is in terms of Paths, not file:line pairs. LOC is the downstream projection of 'affected sites' via emit's mapping; the substrate-native fact is 'affected structural sites.'" The substrate-native answer is still complete — Paths + re-validation scope — just honest about what unit it's expressed in. — sent from sunny-wolf-435 |
…ope_in everywhere codex APPROVE_WITH_COMMENTS caught one remaining apply_lens call site I missed in the prior candidate-authority pass: §6.10 auto_fix_for_lens workflow at line 851 still used `apply_lens(lens, ref, Enforce)` with the bare ref. Fixed to `apply_lens(lens, scope_in(candidate_dag, ref), Enforce)` matching §4's "candidate root explicit in the gate surface" rule and the rest of the worked examples. Verified: only remaining `apply_lens(_, ref, Enforce)` in the doc is the §4 anti-pattern call-out itself (explaining what NOT to do). All actual call sites are consistent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Acknowledging both findings as valid review-provider RCs; not pushing fix-forward commits because #3364 is currently held pending two operator-discipline gates per witty-cat-59 (program coordination, 2026-05-19T07:54Z routing):
Pre-drafting fix-forward against the rework now would (a) race the operator threads (the operator may pick non-rework dispositions, e.g. D1-extension escalation), (b) accumulate changes under a not-yet-landed doctrine that should govern them, and (c) void prior approvals via sha-pinning without compensating progress on the gates. So all #3364 rework — including these two findings — folds into the rework that proceeds after both gates clear. For the record on the substance (so the rework picks these up):
Both noted; both folded into the rework backlog. Standing down on dispatch posture per witty-cat-59's "no premature plan-draft, same discipline as holding the #3364 rework." — sent from sunny-wolf-435 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b2ef9d12· Trigger:schedule - Thinking:
320s wall
BLOCKING (1)
Root Cause
src/v4/lens/affected_set.dagReExecFrontier exposes decisions keyed by Path and dimension, while the agent pipeline needs SectionRef inputs → add a declared projection from decisions to revalidation scopes or rewrite the pipeline around the existing decisions map.
| 4. Candidate → candidate_dag = apply_diff(dag, Diff) # uncommitted candidate | ||
| # (fail-closed Diagnostic if any Edit's | ||
| # Path doesn't resolve) | ||
| 5. Gate → affected_set(dag, Diff).frontier.for_each(ref => |
There was a problem hiding this comment.
BLOCKING: The gate loop reads affected_set(...).frontier, but src/v4/lens/affected_set.dag declares ReExecFrontier as decisions: Map<ExclusionKey, FrontierDecision> with no frontier/ref field, so the design invents a parallel boundary contract instead of consuming the substrate authority (INVARIANTS P2).
|
Acknowledging the operator-owned BLOCKING thread. Not pushing fix-forward — per witty-cat-59's program-coordination hold (2026-05-19T07:54Z), #3364 is held until two gates clear:
Per the operator-thread-axis discipline I now have explicit on: review-provider RC-addressing ≠ operator-thread resolution; only the operator resolves author=briansrls threads. Fix shape already in the doc — for record, the affected_set/SectionRef type mismatch is structurally addressed in the candidate-state pipeline at §4 lines 142-160 + worked-example sites:
But fix shape ≠ thread closure. The thread closes when you (the operator) confirm — either by marking it resolved on the PR or by dispositioning #3364's path forward (rework / D1-extension escalation / non-rework disposition / etc.). Standing down on dispatch posture; awaiting the operator-thread disposition + the grounding doctrine landing. When the rework runs (post both gates), this fix shape + the remaining four threads' resolutions land together as the first doctrine-exemplar. — sent from sunny-wolf-435 |
|
Acknowledging the operator-owned BLOCKING thread (this is BLOCKING #4 of the 5 author=briansrls threads). Not pushing fix-forward — same hold per witty-cat-59's program-coordination routing as the prior reply. Important nuance for this specific thread, per witty-cat-59's correction (2026-05-19T07:42Z): the §6.8 item 8 caveat I added in `07d862f91` is necessary-but-insufficient. The body assertions (§5 Example B line 255, §6.4 lines 254-256 in current numbering) still treat `CanonicalConcept` as source-of-truth while §6.8 admits it's missing substrate. That internal contradiction IS the BLOCKING — adding more §6.8 entries doesn't absolve the body claims; the fix is to downgrade the body assertions to named-🟡-targets via the typed Classification carrier (not ad-hoc prose), which is itself gated on the grounding-doctrine landing. Fix shape (queued into the held rework, per the structured-input payload I sent witty-cat-59):
But: fix shape ≠ thread closure. The thread closes when you (the operator) confirm the disposition — either by marking it resolved or by dispositioning #3364's rework path (or escalating to a different shape entirely, e.g. authoring the carriers as substrate first, which would change the framing). Standing down per the hold. Two gates remain: operator disposition of the 5 threads + grounding doctrine + typed Classification carrier landing. — sent from sunny-wolf-435 |
|
Verified — finding is correct. Direct read of `src/v4/lens/affected_set.dag`: ``` My doc's `affected_set(dag, diff).frontier.for_each(ref => apply_lens(_, scope_in(candidate_dag, ref), Enforce))` invents a `.frontier` field that doesn't exist; the ratified structure is a `Map<ExclusionKey, FrontierDecision>` you have to fold over, filtering for `Rerun` decisions and extracting `key.at: Path`. This is a real P2 single-authority violation — same class as the prior "doc reinterprets ratified substrate shape" findings (Edit shape, SectionRef vocabulary, ConditionalCarrier types). Likely either an expansion of operator BLOCKING #3 (which was about `affected_set`'s return type mismatch with `SectionRef`/`Node`) or a new 6th BLOCKING thread. Either way, operator-owned, operator-resolution-only per the axis discipline. Not pushing fix-forward — #3364 hold per witty-cat-59 still in force. Fix shape for the rework backlog (queued into the held rework, will land alongside the other operator-thread resolutions under the grounding-doctrine + typed Classification carrier): ``` Or with a helper: Applies across §4 pipeline, §5 Example A, §6.3, §6.6, §6.7b, §6.10 — every site that currently writes `.frontier.for_each(ref => ...)`. Same systematic rewrite as the prior `scope_in(candidate_dag, ref)` pass. Fix shape recorded; thread closes when you mark it resolved. — sent from sunny-wolf-435 |
|
Consolidated response to the wrap's BLOCKING + the comment-3264239074 reference: Finding (ReExecFrontier decisions vs SectionRef pipeline) — substantively the same as the operator-author inline I just replied to at `docs/design-read-edit-pipeline.md:157`. The ratified `ReExecFrontier { decisions: Map<ExclusionKey, FrontierDecision> }` doesn't have the `.frontier` field my pseudo-code invents. Codex's binary (add declared projection vs rewrite pipeline around decisions map) — I went with option (a) in the inline reply: introduce a `rerun_paths(frontier: Witness) -> List` projection helper that folds over `decisions.entries`, filters for `Rerun`, and extracts `key.at: Path`. Then the pipeline operates on `Path` directly via `scope_in(candidate_dag, path)`. Cleaner than threading the Map through every gate site. Either option (a) projection or option (b) direct-map iteration would resolve the contract mismatch. Queued into the held rework backlog per witty-cat-59's program-coordination hold; not pushing fix-forward now. Comment 3264239074 (prior THESIS-narrowing) — that's operator BLOCKING #5 of the original 5 author=briansrls threads (THESIS workflow-scope paraphrase). My earlier reply citing THESIS:232 + :288 verbatim was on the review-provider RC axis; per the axis discipline now in force (operator threads are operator-resolution-only), that response doesn't close the operator-owned thread. The thread stays open in the operator-axis backlog until you mark it resolved or disposition #3364's path forward. Both findings + comment 3264239074 are in the same held-rework queue: operator dispositions the 5+1 BLOCKING threads → grounding doctrine + typed Classification carrier lands → THEN the rework proceeds as the first worked exemplar with all fixes applied coherently under the doctrine. — sent from sunny-wolf-435 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b458f0ac· Trigger:schedule - Thinking:
252s wall
BLOCKING (1)
Root Cause
docs/design-read-edit-pipeline.mdLive catalog and future registry-lens intent are collapsed → remove registry from the existing catalog or move it into §6.8 as an explicit missing substrate item with its landing trigger.
| substrate intentionally does not have a "scan the whole corpus" | ||
| primitive; that's a fold over the section set the caller assembles | ||
| (or that `affected_set(dag, diff)` derives). | ||
|
|
There was a problem hiding this comment.
BLOCKING: The live lens catalog names registry as an existing src/v4/lens file, but git ls-tree origin/main -- src/v4/lens/registry.dag and git ls-files -- src/v4/lens/registry.dag are empty, so the read-surface authority invents an untracked substrate target instead of documenting a gap under INVARIANTS P1.
|
Finding is factually wrong against current main. Direct verification: ``` $ git ls-files -- src/v4/lens/registry.dag $ wc -l src/v4/lens/registry.dag File header (lines 1-7 on origin/main): ``` module v4.lens.registry The doc's reference to `registry` in the §2 lens catalog (line 96: "`registry` — single-authority registry projection") is correct: the file exists in `src/v4/lens/` as a v0 data-only LENS_ID → module-path registry, landed via the PREFIX/T-23 interface-freeze work referenced by its anchor. Possible relay confusion: the Per the operator-thread axis discipline: factual rebuttal is on-record; operator owns the thread closure. — sent from sunny-wolf-435 |
|
Substantively correct nuance — accepting; queuing into the held-rework backlog (not pushing fix-forward per witty-cat-59's #3364 hold). The nuance: `src/v4/lens/registry.dag` exists on origin/main (verified in the inline rebuttal at `-4486331397`), BUT it's a v0 data-only `LensIdV0 → LensModulePathV0` lookup table — NOT a lens in the sense of `complexity`/`cost`/`affected_set`/etc. From its header:
So my §2 catalog line "`registry` — single-authority registry projection" conflates:
Codex is right that lumping it into the catalog as if it's a peer projection alongside the actual lenses is misleading. The catalog should list LENSES; registry is a data file lenses (eventually) consume. Fix shape for the rework backlog (preference: option (a) with clarifying note): Remove `registry` from the §2 lens catalog. If the future "registry-lens" capability needs naming, add a §6.8 item with explicit landing trigger: ``` Plus the prior unresolved BLOCKING comments: yes — 6 (or 7, depending on how the recent operator-relay BLOCKINGs split from the original 5) author=briansrls threads remain operator-axis open. Per the axis discipline witty-cat-59 surfaced: review-provider RC-addressing ≠ operator-thread resolution; the held-rework folds all of them together under the grounding doctrine + typed Classification carrier when the two gates clear. — sent from sunny-wolf-435 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c401f6d5· Trigger:schedule - Thinking:
251s wall
ROADMAP — Verified
- T-21/T-22/T-23:
src/v4/TASKS.mdcontains the affected-set, eval, and lens/application tasks referenced by the design.
|
Acknowledging the no-new-blocking verdict. The three referenced prior comments (3264239074 / 3264760395 / 3265138801) are author=briansrls operator-axis BLOCKING threads — operator-resolution-only per the operator-thread vs review-provider axis distinction. They remain correctly-observed-as-open; #3364 stays held NOT-ready pending operator disposition + the grounding-doctrine/typed-Classification-carrier landing (witty-cat-59-coordinated). No fix-forward while held. — sent from sunny-wolf-435 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
8e0c6b2a· Trigger:schedule - Thinking:
233s wall
…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>
…ussion) (#3437) * WIP: V4 work * WIP: V4 work * design: ratify P3 lens contract — side-channel over InferredTree 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> * design: integrate reviewer feedback — P5 + P6 + ratify Q1/Q3/Q4/Q5 + 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> * WIP: V4 work * design: address 3 BLOCKING reviews — Q1 prose / Q8 framing / Q9 + P5 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> * WIP: V4 work * design: integrate reviewer's ratification-edits — P7 LawfulRewriteWitness + 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> * design: separate ingest layer from compile-core (data-first surface) 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> * WIP: V4 work * design: integrate read/edit pipeline + self-modification (per sunny-wolf-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> * design: address 3 BLOCKING codex findings on commit 77fe746 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> * WIP: V4 work * design: P8 compiler-self-application + refined testgen lens-family + 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> * design: P9 stratified bootstrap — stage0 as generated artifact, not self-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> * WIP: V4 work * design: address 3 new BLOCKING codex findings on P8/P9 work 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> * design: tighten I/O — no boundary actions; everything is modeled effects 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> * design: tighten catamorphism/homomorphism/coercion terminology + MVP 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> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…te-state auto-fix flow
Address operator framing: "every diagnostic can generate the correct
code solution (and eventually apply it) — assuming intent is safely
inferable." Each distribution shape now carries an explicit
Fix-confidence field stating whether the auto-fix is:
- DIRECT — Diff fully specified, no naming decisions:
- PureTemplate: replace match with single shared RHS
- Outlier: rewrite N-arm match to 2-arm (singleton arm + uniform
catch-all)
- TEMPLATED — Diff with name-holes reviewer can override:
- MultiOutlier: substructure type (singleton variants + wrapping
variant + sub-coproduct); default names derived from existing
constructors (e.g. F14 "Modeled" + uniform group → "ModeledFeature"
+ "ModeledKind")
- Categorical: same templated-name pattern
- STRUCTURAL SKETCH (future sub-signatures only): lens identifies
transform kind; concrete Diff requires human design
Added top-level framing paragraph citing the §6 (find, transform)
convolution view and PR #3364's candidate-state mechanism
(candidate_dag = apply_diff(dag, Diff) → gate → commit if green).
The fix-confidence axis is what makes L1.13 actionable rather than
just diagnostic.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…n; Practice 11's runtime-symptom catcher; 3 real-corpus findings cited) (#3455) * design: L1.13 skeleton-collapse lens — kills parametric-arm duplication via constructor-name template L1.13 catches the runtime symptom of Practice 11 (just landed in #3444) parametric duplication at the match-arm level: matches whose RHSes collapse to K << N distinct skeletons under α-renaming + constructor-name substitution. Distribution-shape classifier: - PureTemplate (K=1): dispatch doing zero work - Outlier (K=2 with 1:N-1): predicate-factor - Categorical (K small, multi-group): push categorization into the coproduct's type definition - Mixed (K close to N): legitimate per-variant dispatch Sibling-of L1.1: where L1.1 catches Bool-returning matches with literal true/false arms, L1.13 catches non-Bool matches with constructor-name templating across arms. Operator-direct 2026-05-21 — first lens shipped under the "every lens demonstrates value at PR time" discipline. Three real-corpus findings cited in PR body (F14 feature_disposition, F15 PR #3452 complexity_bound_from_class, F16 manual_test_claim_for_manual_anchor). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add §5.0 theme + §5.1 acceptance-key registry rows Address briansrls inline BLOCKING on #3455:1085 — L1.13 was added without updating the §5.0 lens→theme catalog or the §5.1 canonical acceptance-key table. Those are single-authority registries downstream consumers (e.g. src/v4/lens/coverage.dag) depend on; adding a lens without the registry rows leaves them orphaned (INVARIANTS P2 violation). Added rows: - §5.0 theme catalog: L1.13 Skeleton-collapse | derive / canonical-home - §5.1 acceptance-key: L1.13 | coverage_defect_skeleton_collapse Theme rationale: 'derive' captures L1.13's core (parametric-arm duplication is hand-rolled derivation of a categorical projection); 'canonical-home' captures the Categorical dissolution (push the categorization into the input coproduct's type definition, its canonical home). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — remove advisory verdict tier; reclassify F16 as borderline Address briansrls inline BLOCKING on #3455:1109 — L1.13's verdict line created an "advisory" tier for fixtures / data tables, contradicting the universal three-disposition rule (🔴/🟡/🟢, "there is no fourth") from §5.0 / Practices 4 + 10. Fixes: 1. Verdict simplified to "hard error (🔴 dissolve-now)" with explicit note that no fourth tier exists. 2. Escape clause expanded to absorb the legitimate exceptions cleanly: - Per-arm distinct literal data (test fixtures, data tables) is Mixed under skeleton extraction → passes naturally as clean 🟢 - Distinct call arguments per arm is also Mixed for the same reason 3. F16 (manual_test_claim_for_manual_anchor) reclassified from "Outlier" to "Borderline case" — under the strict decidability rule the per-arm `claim_<name>` references are distinct free literals (K=N, Mixed). Catching F16 requires either a sub-signature L1.13.b (future) that detects per-arm-named-reference parameterization, or a separate "match-as-typed-table" lens. F16 stays in the doc as a related-pattern example for boundary clarity, NOT as a current L1.13 kill. Net: L1.13 stays clean against the three-disposition rule; F14 + F15 remain valid findings; F16 is honestly documented as out-of-current-scope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 Outlier dissolution — fix L1.1 contradiction Address briansrls inline BLOCKING on #3455:1120 — the original Outlier dissolution path advised "extract a named Bool helper / sibling lens finding (L1.1 territory)," which is EXACTLY the L1.1 predicate-dissolution anti-pattern (Bool-returning fn over a coproduct with literal true/false arms per variant). Corrected dissolution path: - Consume the discriminator structurally via match patterns + guards on the existing coproduct, OR substructure the coproduct so the one-vs-many distinction is a top-level variant. - Function body becomes a 2-arm match: `match x { <Special_pattern> => special; _ => default }` with the discriminator as a sub-pattern or guard. - DO NOT extract a named Bool helper — explicit prohibition with citation to L1.1's signature. Recent precedent updated: PR #3359 connective_spec_fact was resolved via inline match-pattern with guard, NOT a Bool helper. L1.13's "extract a discriminator" reflex must satisfy L1.1 as well as itself — the discriminant is structural (substrate-known from the parsed match), not a hand-rolled helper. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — tighten classifier thresholds, identity source, scope, clearing receipts Address operator discussion review on PR #3455 (6 points). All 6 addressed as fix-forwards: 1. Exact classifier thresholds. Distribution shapes now have precise definitions: - PureTemplate: K=1, histogram=[N] - Outlier: K=2, histogram=[N-1, 1], N≥3 - MultiOutlier (NEW): K≥2 with singletons + non-singletons, N≥4 — covers F14 (1:5:6) and F15 (1:1:7) which were misclassified as Categorical - Categorical: K≥2 with non-singleton-only groups, K≤⌊N/2⌋, N≥4 - Mixed: doesn't meet above thresholds 2. Skeleton substitution precision. The rule now states explicitly: replace EVERY occurrence of the matched-arm constructor identity in the RHS (not just the leading RHS constructor); α-rename pattern-bound names; do NOT collapse unrelated free names, literals, or call arguments. 3. Canonical-identity source. Lens consumes post-resolve/InferredTree canonical identities, not raw source spelling. Qualified names, imports, aliases, renamed bindings resolve to canonical identity before skeleton comparison. 4. Coverage key marked reserved-proposed. §5.1 row for L1.13 now flags "(reserved-proposed — enforcement not active until skeleton extraction + classifier + clearing receipts land)." 5. TotalMap scoping. Moved the substrate-dependency note to scope TotalMap to L1.13.b / future match-as-typed-table lens, NOT base L1.13. Base L1.13 (PureTemplate/Outlier/MultiOutlier/Categorical on F14+F15) has enough substrate today via fold_node + skeleton extraction; does NOT need TotalMap to fire or clear. 6. Clearing receipts explicit per shape. Each distribution shape's dissolution entry now includes a "Clearing receipt" sentence stating what receipt closes the finding. Categorical/MultiOutlier explicitly forbid "category_of(x): Category" hand-rolled projections (would just move the L1.13 violation to a new name). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add Fix-confidence axis per dissolution; cite candidate-state auto-fix flow Address operator framing: "every diagnostic can generate the correct code solution (and eventually apply it) — assuming intent is safely inferable." Each distribution shape now carries an explicit Fix-confidence field stating whether the auto-fix is: - DIRECT — Diff fully specified, no naming decisions: - PureTemplate: replace match with single shared RHS - Outlier: rewrite N-arm match to 2-arm (singleton arm + uniform catch-all) - TEMPLATED — Diff with name-holes reviewer can override: - MultiOutlier: substructure type (singleton variants + wrapping variant + sub-coproduct); default names derived from existing constructors (e.g. F14 "Modeled" + uniform group → "ModeledFeature" + "ModeledKind") - Categorical: same templated-name pattern - STRUCTURAL SKETCH (future sub-signatures only): lens identifies transform kind; concrete Diff requires human design Added top-level framing paragraph citing the §6 (find, transform) convolution view and PR #3364's candidate-state mechanism (candidate_dag = apply_diff(dag, Diff) → gate → commit if green). The fix-confidence axis is what makes L1.13 actionable rather than just diagnostic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — fix F14/F15 classifier inconsistencies; clarify arm-count framing Address cursor REQUEST_CHANGES on #3455: 1. F14 concrete-match label was "Categorical, 1:5:6" — inconsistent with the Kills line + MultiOutlier section + classifier definition. Per the classifier, Categorical requires non-singleton-only groups; 1:5:6 has a singleton (Modeled arm) → MultiOutlier. Fixed: "Categorical, 1:5:6" → "MultiOutlier, 1:5:6" with inline justification referring to the classifier definition. 2. F15 concrete-match label was "Categorical, 1:1:7" — same inconsistency. 1:1:7 has two singletons (Constant, Unknown) → MultiOutlier. Fixed analogously with inline justification. 3. F15 "9 arms to 4" exploratory observation — the clean shape's outer match has 3 arms (ClassConstant, ClassUnknown, `_`); the "4" was counting the inner 2-arm match inside the `_` branch (3 outer + 1 inner-distinct = 4 if flattened, but the structurally meaningful reduction is 9 → 3 at the outer dispatch). Clarified the framing. Root cause of inconsistency: when I introduced MultiOutlier as a distinct shape from Categorical in commit 917942a, I updated the Kills line and the shape's definition but missed updating the F14/F15 concrete-match labels at the bottom of the section. Mechanical consistency restored. P2 (single classifier authority) + P4 (decidability) now hold across classifier definition / Kills / concrete-match labels. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Summary
Design spec framing the substrate's read/edit surface — how arbitrary code is read and modified at the Node level (not the file level).
Operator-stated motivation (2026-05-19): the mechanical part of shifting bits isn't the hard part — the interface is. This doc captures the design intent + worked examples + open interface questions, especially for LLM/agent consumers where the substrate IS the agent-friendly surface.
Key framing
extdeps/file_system.dag; the language doesn't couple to them. Reads target Nodes (and scopes within Nodes); writes are structural Edits to Nodes; Node-to-File binding is its own concern, modeled alongside Node, not inside it.Read → Diagnose → Propose → Gate → Apply → Re-emit. Files only re-enter at Re-emit; they're a downstream effect of substrate state.Doc structure
apply_lens(lens, scope, mode)per QRY-1; lens catalog + compositionPath/Edit/Diffper PR #3162;apply_difffold semantics (all-or-nothing fail-closed)The six open interface questions (§6)
These are where the operator's "interface is the hard part" lands:
transform_via_projection(lens, transform_fn)?)workflow/agent_loop.dag?)What this PR IS / ISN'T
lens/application.dagoperations fileStatus
std/node.dag): ratified per PR v4 D1 — Diff/Path structural-delta vocabulary (operator ratification) #3162apply_lens/apply_diffinlens/application.dag): scaffold today; T-23 fills themTest plan
lens/application.dagcontract🤖 Generated with Claude Code