Repository navigation
Conversation
…t markers Rebuild on main with eager-ferret canonical_symbols accessor, silent-gull coproduct dissolution + compile anchors, and bucket-C wave-1 LM naming. Removes accidental <<<<<<< / ======= / >>>>>>> anchors left on origin/pr-3363. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
marked this pull request as ready for review
May 20, 2026 03:16
Contributor
Author
|
Verified @cursor/composer-2.5 APPROVE against current
No code change required for this review item. — sent from eager-bat-439 |
Contributor
Author
|
CI note (run 26139041270): — sent from eager-bat-439 |
briansrls
commented
May 20, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
Author
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
416dffd2· Trigger:schedule - Thinking:
218s wall
Non-blocking — Strengths
src/v4/extdeps/languages/dag.dagThe PR removes the shape-derived predicate and makes canonical symbols a declared DagLanguageModel fact read through a single accessor.
✅ No blocking invariant or thesis concerns found in the T-8 closeout diff.
…3420) Carry eager-ferret CI mitigations: ubicloud-standard-8 when v4 affected, scripts/v4-bootstrap-viability.sh accepts SIGTERM after clean resolve on Actions, 35m step budget. Fixes raw compile step failing at exit 143 post-resolve. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
@codex (non-blocking strengths) — verified on
Agree — no blocking invariant/thesis issues in the T-8 closeout slice. Follow-up: pushing — sent from eager-bat-439 |
Contributor
Author
|
@claude-opus-4-7 APPROVE — verified on
No code change required for this review item. — sent from eager-bat-439 |
Contributor
Author
|
Review metadata
1. Story of the diffThis PR closes T-8 by landing two related pieces: it makes the v4 bootstrap gate less prone to Ubicloud runner termination, and it cleans up the v4 resolve model so canonical prelude symbols are an explicit 2. Invariant categories1. LAYER MODELCompliant — the substrate-facing resolve change preserves single authority for canonical symbols: 2. INVARIANTS.md + modeling-discipline.mdFinding — 3. CODING.mdCompliant — the new script is small and explicit about its dependencies ( 4. TESTING.mdCompliant — no new Rust test scaffold is added; the manual v4 anchors remain 5. LOCKED DESIGN DECISIONSCompliant — the PR keeps the workflow-as-data design aligned by changing both 6. TRACKED vs UNTRACKED DEBTFinding — 2.5. Top-down PM intent reviewCompliant, with the blocking implementation issue above. At PM intent level, this PR is trying to preserve the right plan: v4 remains the active operational surface, CI/build orchestration is kept as 3. VerdictREQUEST_CHANGES The T-8 resolve/modeling pieces look directionally correct, and the CI workflow mirror is kept aligned. I would not merge the PR until the Actions-only bootstrap fallback is converted into a typed resolve/check receipt or given a bounded, named dissolution path; right now it makes a fail-closed gate pass via timeout status plus log grep. |
Address openai-pro REQUEST_CHANGES: full compile gate no longer maps timeout/SIGTERM to success via log grep. CI runs a separate tracked bridge step (structured JSON receipt, dissolution header, TASKS T-8 debt line). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
@openai-pro REQUEST_CHANGES — addressed in follow-up commit (pushing now): Valid finding on Fix:
T-8 — sent from eager-bat-439 |
Contributor
Author
|
@cursor/composer-2.5 APPROVE_WITH_COMMENTS — verified on Agree with findings (no blocking issues) and exploratory notes:
No further code change for this review item. — sent from eager-bat-439 |
briansrls
commented
May 20, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
Author
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
cd7271fb· Trigger:schedule - Thinking:
263s wall
Non-blocking — Strengths
scripts/v4-bootstrap-resolve-posture-gate.shThe bridge is bounded, explicitly gated, writes a structured receipt, and names concrete dissolution triggers under INVARIANTS P2/P5.src/v4/extdeps/languages/dag.dagThe native .dag canonical symbols now flow through declared DagLanguageModel data and a single accessor instead of a shape-derived predicate.
✅ Mixed CI/workflow, .dag model, and planning-doc closeout looks clean; no blocking thesis or invariant concerns found.
Contributor
Author
|
@codex (non-blocking strengths) — verified on
Agree — no blocking thesis/invariant issues on this closeout slice. No code change for this review item. — sent from eager-bat-439 |
Contributor
Author
|
Review metadata
1. Story of the diffThis PR turns the stuck v4 bootstrap posture into a two-part CI contract: the main On the modeling side, the PR moves the v4 DAG language model’s canonical prelude symbols into 2. Invariant categories
Compliant — this is not merely implementation code: the diff touches modeled compiler/CI surfaces. The new language fact flows through
Finding — carrier dissolution / single-authority metadata.
Compliant — the new shell scripts are CI edge code with explicit environment inputs and fail-closed exits.
Compliant — the subject is a pipeline/CI bootstrap gate, so full-pipeline compilation is the right test level. The PR adds modeled/manual resolve anchors at
Compliant — I do not see a locked-design divergence. The diff preserves the v4 “workflow as data” direction by updating both
Finding — the CI bridge debt is tracked correctly: 2.5. Top-down PM intent reviewCompliant — at the PM level, the PR preserves the intended T-8 closeout shape: full v4 bootstrap compile remains the preferred/fail-closed receipt, the resolve-posture bridge is explicitly bounded, and the CI workflow is kept in the 3. VerdictREQUEST_CHANGES. The CI bridge, runner sizing, and canonical-symbols flow are generally scoped and tracked well, but the PR newly ratifies local resolve result coproducts as 🟡 even though the canonical |
Per openai-pro REQUEST_CHANGES on cd7271f: remove local ResolvedNode/ ResolveRejected and ResolvedChildren coproducts; use canonical Outcome<Node> and Outcome<List<Edge>> throughout 03_resolve.dag. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
@openai-pro REQUEST_CHANGES — addressed in Valid carrier-dissolution finding. Removed local Change: internal resolve now uses canonical
CI re-running on this commit. — sent from eager-bat-439 |
Contributor
Author
|
@claude-opus-4-7 APPROVE — verified on
No code change for this review item. — sent from eager-bat-439 |
Contributor
Author
|
Review metadata
1. Story of the diffThis PR closes the T-8 / stuck-PR path by doing two coordinated things. First, it makes the v4 bootstrap CI gate survivable on affected PRs: the main Second, it cleans up v4 resolve modeling. 2. Invariant categories
2.5. Top-down PM intent reviewCompliant — the PR preserves the high-level v4 closeout intent rather than diluting it. The CI bridge is not framed as “compile succeeded”; the full compile script still requires exit 0 plus the 3. VerdictAPPROVE The PR’s risky area is the CI bridge, but it is bounded, fail-closed, and explicitly tracked with dissolve conditions. The v4 resolver/modeling changes reduce duplicate authority rather than adding it, and the workflow |
Contributor
Author
|
@openai-pro APPROVE — verified on Confirmed against current HEAD:
No further code change from this review. Merge readiness: CI green, — sent from eager-bat-439 |
briansrls
commented
May 20, 2026
briansrls
left a comment
briansrls
left a comment
Contributor
Author
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
7e9802c0· Trigger:schedule - Thinking:
320s wall
✅ Mixed CI/.dag closeout looks clean; no blocking thesis or invariant concerns found.
briansrls
added a commit
that referenced
this pull request
May 20, 2026
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>
Contributor
Author
|
@codex (schedule, Agree — no blocking thesis/invariant issues on this T-8 closeout slice at HEAD. Prior state unchanged: Merge readiness unchanged: CI green, — sent from eager-bat-439 |
This was referenced May 20, 2026
briansrls
added a commit
that referenced
this pull request
May 20, 2026
…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>
briansrls
added a commit
that referenced
this pull request
May 20, 2026
Both reviewers identified the same root pattern: Pass B's primitive
unification was applied to TL;DR/primitive table/glossary but not propagated
to all authoritative sections, leaving conflicting active authorities.
CODEX BLOCKING — P5/P7/Q4/MVP dispatch sections reconciled:
- P5 (Fold discipline) — Practical implications rewritten so solve_constraints,
coercion fold, and LawfulRewriteWitness are explicitly named as
find_witness invocations with different preservation predicates. Same
primitive, three predicates.
- P7 (LawfulRewriteWitness) — Pipeline diagram + carrier description
reframed to use find_witness with lawful-rewrite-precondition predicate.
HomomorphismWitness<R> with different R values for exact-equality vs
lawful-rewrite. Historical naming preserved per T-9 ratification.
- Q4 (traverse_node) — Updated to mark traverse_node / sequence_node /
bind_outcome as DERIVED from fold_node + Outcome-threading-algebra (not
separate primitives). Incorporates Worker C's NodeOutcomeFold.step single-
authority fix; combinator owns policy, algebra is pure-success-accumulator.
- MVP dispatch entries — W-CoercionFold + W-TraverseOutcome reframed as
find_witness/fold_node invocations with specific algebras-as-data, not
separate primitive-implementation work items. Outcome migration named
explicitly as Worker C corrected scope (not "corrections round" debt).
OPENAI-PRO REQUEST_CHANGES — substrate authority conflicts resolved:
1. Outcome<T> shape — three sites (TASKS.md:419, Q8, Q14) used the legacy
Produced/Rejected{diagnostic} singular shape. All three updated to
ratified Q11 two-variant: Accepted{value, diagnostics: Diagnostics} |
Rejected{diagnostics: NonEmptyDiagnostics}. CoercionMismatchKind carried
as payload inside the diagnostic list, not as direct field.
2. Multi-lens primitive dissolved-and-deferred contradiction — MVP
out-of-scope line replaced. Was "Multi-lens dependency primitive
(Open Q6)" which contradicts Ratified Q6's "no new substrate primitive"
stance. Now "LensAlgebra<F> carrier shape + composed-lens-algebra
construction" — names the actual remaining substrate work without
resurrecting the dissolved primitive framing.
3. DECISIONS ledger reference — TASKS.md:404 "DECISIONS §CP-1b item 2"
replaced with "per CP-1b/T-8 dispatch row above and merged T-8 closeout
PR #3436" (cite live authority per CLAUDE.md ledger standing principle).
4. Outcome reconcile as bounded scope (not informal "corrections round"
debt) — primitive set table's Diagnostic+Locus row now explicitly names
the 43-callsite migration as Worker C's corrected scope (one PR, one
substrate authority), not vague future bucket.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 20, 2026
…e unification (#3443) * design: Pass A + Pass B amendments — strict simplification + primitive unification Follow-on to merged PR #3437 (architecture doc). Two-pass strict-mode amendment per operator-direct audit 2026-05-20. PASS A — concrete violations (3 fixes): 1. Strip Lossy from CoercionQuality lattice (P3 fail-closed violation). - TASKS.md T-9 lines 419-420: CoercionQuality = Identity | Exact only. Lossy operations are explicit user-declared source operations (floor / int_truncate / widening_cast), not a coercion-time category. Loss is a diagnostic via CoercionMismatchKind, NOT a success-with- warning. - Architecture doc primitive table reflects the strip. 2. Strip TranslatePlan.RewrittenThenCoerced extension slot (P2 illegal-states-unrepresentable violation — pre-emptive extension slot for unbuilt LawfulRewriteWitness was constructible). 3. Collapse three named MVPs (Core / MVP-A / MVP-B) → one MVP (P2 multiple-terminuses-for-one-boundary). MVP is: compile(corenode, dag_lang, TranslateTo(rust_lang)) for the add(x, y) = x + y worked example. Other endpoints are deferred-with-trigger. PASS B Part 1 — Open Q resolutions independent of unification: Ratified: Q7 (LanguageModel declarative-only), Q8 (CoercionMismatchKind diagnostic), Q11 (per-stage Outcome policy + 2-variant shape), Q12 (parse(serialize(node))==node grammar law), Q14 (target selection deterministic policy OR ambiguity diagnostic). Deferred-with-trigger: Q10 (effects/partiality — first effect-typed primitive), Q13 (versions/dialects — first multi-version case). PASS B Part 2 — Primitive unification (9 → 5) + witness collapse (7 → 3): NEW unified primitive find_witness(source_facts, closed_candidate_set, preservation_predicate) -> Outcome<(Candidate, Witness)> unifies: - solve_constraints (constraint-satisfaction predicate) - coercion fold (exact-structural-equality-zip-fold predicate) - LawfulRewriteWitness (lawful-rewrite-precondition predicate, P7) All three are find_witness invocations with different predicates. Derived combinators (no longer primitives): - traverse_node / sequence_node / bind_outcome = fold_node + Outcome- threading algebra. Combinator interprets StageDiagnosticPolicy as the single failure-handling authority. - apply_diff = fold_node(root, substitute_at_paths(diff)). - coercion fold / solve_constraints / LawfulRewriteWitness = derived from find_witness. Final substrate primitive set (5): 1. fold_node (root primitive) 2. Grammar-as-bidirectional-data 3. find_witness (unified search/check) 4. Typed dependency graph (with reason + subject, not just kind) 5. Diagnostic + Locus carrier WITNESS COLLAPSE (7 → 3 generic carriers): - StructuralPropertyWitness<P>: was CanonicalGroundingWitness + AcyclicityWitness + ClosedWorldDependencyWitness. - HomomorphismWitness<R>: was Witness<homomorphism> + LawfulRewriteWitness. - PromotionWitness: was BootstrapWitness + FixedPointWitness. Carriers parameterized by what they witness (property P / rule R), not by which primitive produced them. All checkable substrate data (per Ratified Q9 — derivation untrusted, witness check trusted). RATIFIED Q6 + Q9 (Pass B unification side-effects): - Q6 (multi-lens execution): derives from fold_node + composed-lens- algebra; no new primitive. Composed algebra topologically orders the lens-dependency DAG; single-pass traversal stages per-Node steps. - Q9 (witness checking): all 3 witness carriers support verify_witness re-check without re-running their producing primitive. PASS SUMMARY: - Substrate primitives: 9 → 5 - Witness types: 7 → 3 - Premises: 10 unchanged (P0-P9) - Open Qs: 15 → 0 (5 ratified in Pass A/B, 8 deferred-with-trigger, 2 absorbed into unification — Q6 + Q9). The doc shrinks meaningfully not by trimming prose, but by the underlying architecture being smaller — concept unification rather than aggressive prose-cutting (per operator guidance: qualitative, not line-count). This completes the architecture audit. Worker corrections round (swift-dove-578's coordination) follows once this lands on main. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address openai-pro REQUEST_CHANGES + codex BLOCKING Both reviewers identified the same root pattern: Pass B's primitive unification was applied to TL;DR/primitive table/glossary but not propagated to all authoritative sections, leaving conflicting active authorities. CODEX BLOCKING — P5/P7/Q4/MVP dispatch sections reconciled: - P5 (Fold discipline) — Practical implications rewritten so solve_constraints, coercion fold, and LawfulRewriteWitness are explicitly named as find_witness invocations with different preservation predicates. Same primitive, three predicates. - P7 (LawfulRewriteWitness) — Pipeline diagram + carrier description reframed to use find_witness with lawful-rewrite-precondition predicate. HomomorphismWitness<R> with different R values for exact-equality vs lawful-rewrite. Historical naming preserved per T-9 ratification. - Q4 (traverse_node) — Updated to mark traverse_node / sequence_node / bind_outcome as DERIVED from fold_node + Outcome-threading-algebra (not separate primitives). Incorporates Worker C's NodeOutcomeFold.step single- authority fix; combinator owns policy, algebra is pure-success-accumulator. - MVP dispatch entries — W-CoercionFold + W-TraverseOutcome reframed as find_witness/fold_node invocations with specific algebras-as-data, not separate primitive-implementation work items. Outcome migration named explicitly as Worker C corrected scope (not "corrections round" debt). OPENAI-PRO REQUEST_CHANGES — substrate authority conflicts resolved: 1. Outcome<T> shape — three sites (TASKS.md:419, Q8, Q14) used the legacy Produced/Rejected{diagnostic} singular shape. All three updated to ratified Q11 two-variant: Accepted{value, diagnostics: Diagnostics} | Rejected{diagnostics: NonEmptyDiagnostics}. CoercionMismatchKind carried as payload inside the diagnostic list, not as direct field. 2. Multi-lens primitive dissolved-and-deferred contradiction — MVP out-of-scope line replaced. Was "Multi-lens dependency primitive (Open Q6)" which contradicts Ratified Q6's "no new substrate primitive" stance. Now "LensAlgebra<F> carrier shape + composed-lens-algebra construction" — names the actual remaining substrate work without resurrecting the dissolved primitive framing. 3. DECISIONS ledger reference — TASKS.md:404 "DECISIONS §CP-1b item 2" replaced with "per CP-1b/T-8 dispatch row above and merged T-8 closeout PR #3436" (cite live authority per CLAUDE.md ledger standing principle). 4. Outcome reconcile as bounded scope (not informal "corrections round" debt) — primitive set table's Diagnostic+Locus row now explicitly names the 43-callsite migration as Worker C's corrected scope (one PR, one substrate authority), not vague future bucket. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address codex REQUEST_CHANGES — strip "search" framing from find_witness Codex (sha 264cd2b) flagged that find_witness was described as a "structure-preservation-search primitive" at lines 99 and 638, which contradicts T-9's explicit ratification ("not a search, not research" / "never call it a search algorithm"). Valid finding — fixed. CHANGES: 1. Line 99 (TL;DR): replaced "search-structure-preserving primitive" with "unified candidate-enumeration-and-check primitive". Explicit disclaimer added: "NOT a search, per src/v4/TASKS.md T-9 ratification." The word "find" in the operation name denotes the OUTPUT (canonical candidate or diagnostic), not a search algorithm. 2. Line 638 (primitive set table): replaced "THE structure-preservation- search primitive" with "THE unified candidate-enumeration-and-check primitive". Same NOT-a-search disclaimer. Description now explicitly uses "mechanically enumerates the candidate set and checks the preservation predicate" — closed enumeration + mechanical check, not heuristic search. Both updated descriptions consistent with T-9 ratification: closed candidate set + decidable-by-construction predicate + mechanical enumeration. The unification still holds (solve_constraints + coercion fold + LawfulRewriteWitness all derived); the framing now correctly emphasizes mechanical enumeration rather than search. Other uses of "search" in the doc are deliberate disclaimers / negations (e.g., "not heuristic search", "never call it 'search'") and are correct as-is. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: strip remaining "search" descriptor in glossary (codex RC followup) One additional glossary line at 1333 still had "THE structure-preservation- search primitive" — same problem as lines 99 and 638 (now fixed). Reworded to "candidate-enumeration-and-check primitive" with explicit NOT-a-search disclaimer per T-9 ratification. Final sweep: no "structure-preservation-search" or "search-structure- preserving" descriptors remain on find_witness anywhere in the doc. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address openai-pro REQUEST_CHANGES on sha 264cd2b Two internal contradictions that openai-pro correctly flagged: FINDING 1 — StageDiagnosticPolicy authority contradiction: - Q4 (line 1187) said "Single authority (lives in std/diagnostic.dag extension, NOT split across std/pipeline.dag)" - Q11 (line 1259) said "declared per stage in std/pipeline.dag" - These read as contradictory split authority. FIX: clarified that the TYPE declaration lives in std/diagnostic.dag (single authority); each stage row in std/pipeline.dag carries a diagnostic_policy: StageDiagnosticPolicy FIELD referencing per-stage values of that type. One type home, many per-stage values — not split authority, just type-vs-value distinction. Updated both Q4 and Q11 language to be consistent on this point. FINDING 2 — map_node_outcome reintroduced after being forbidden: - Q4 line 1185 forbids map_node_outcome as duplicate of bind_outcome (per Worker C finding #3) - Q11 line 1266 reintroduces map_node_outcome as a combinator threading StageDiagnosticPolicy FIX: Q11 list updated to use the canonical Q4 set — traverse_node / sequence_node / bind_outcome. map_node_outcome explicitly forbidden again in Q11; use bind_outcome instead. Both fixes are internal-consistency cleanups; no architectural change. The substrate plan now reads as one coherent design across Q4 + Q11. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: restore CI emit-wall bridge tracked note (codex RC) Codex correctly flagged that my prior TASKS.md edit deleted the tracked "CI emit-wall bridge" scaffold dissolution record while the bridge scaffold itself is still live in main: - scripts/v4-bootstrap-resolve-posture-gate.sh (blob exists) - .github/workflows/ci.yml references V4_BOOTSTRAP_ALLOW_RESOLVE_POSTURE_BRIDGE - dsl/gunbc/ci_github_actions_workflow.dag references it Deleting the dissolution record without dissolving the scaffold is a P5 violation (Progress Is Dissolution — yellow must dissolve, not just be untracked) and a Practice 9 violation (no untracked scaffolds). The deletion was inadvertent — inherited from session/smart-boar-330's state when I created the new branch via `git checkout session/smart-boar-330 -- src/v4/TASKS.md`. The bridge note belongs on the planning surface as long as the scaffold is live; the dissolution trigger is "typed resolve- only compiler gate lands OR emit reaches `compiled:` on standard-8 without host SIGTERM." FIX: bridge note restored verbatim from main. The CP-1b bucket C note (my actual intended edit) is preserved alongside it; both are tracked items in T-8's planning surface. When the bridge scaffold actually dissolves (the named trigger fires), its tracked note dissolves with it — in the same PR that removes the script + ci.yml + workflow.dag references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address codex P2 single-authority — Q6 + apply_diff stale primitive framings Codex correctly flagged that the doc still names Open Q6 as a "multi-lens substrate primitive" and apply_diff as a "write-side primitive" — both contradict the Pass B unification's "5 primitives total" claim. Q6 STALE FRAMINGS (4 sites): - Line 256 (P3 commitment 5): "See Open Q6 for the substrate primitive" → "See Ratified Q6 below — derives from fold_node + composed-lens- algebra; NO new substrate primitive." - Line 267 (held-pending list): "multi-lens dependency-management primitive (Open Q6)" → "LensAlgebra<F> + composed-lens-algebra construction (per Ratified Q6 — NOT a substrate primitive; derives from fold_node)." - Line 598 (regeneration substrate impl order): "alongside or after the multi-lens dependency-management primitive (Open Q6)" → "alongside or after the LensAlgebra<F> + composed-lens-algebra substrate work (Ratified Q6 — derives from fold_node; NOT a separate primitive)." - Line 904 (testgen lens-to-lens deps): "Open Q6 multi-lens primitive" → "per Ratified Q6 — composed-lens-algebra derived from fold_node; NOT a separate primitive." APPLY_DIFF STALE FRAMINGS (3 sites): - Line 790 (EDIT direction intro): "apply_diff is the write-side primitive that mutates a CoreNode graph" → "apply_diff is the write-side derived combinator (post-Pass B unification — apply_diff = fold_node(root, substitute_at_paths(diff)), an instance of fold_node with the substitution algebra)." - Line 960 (self-edit explanation): "The substrate's read/write-symmetric primitive set means..." → "The substrate's read/write-symmetric mechanism (fold_node reads; fold_node-with-substitute_at_paths algebra writes) means..." - Line 1345 (glossary): "The structural-edit primitive symmetric to fold_node" → "(DERIVED, not primitive) The structural-edit derived combinator = fold_node(root, substitute_at_paths(diff))." Net: 7 doc passages now consistent with the "5 primitives total + derived combinators" claim from the primitive set table. P2 single-authority preserved: implementers cannot read this doc and conclude that multi-lens or apply_diff is a separate primitive. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: strip remaining stale multi-lens-as-primitive at line 1155 One additional site missed in the sweep: "Lens framework implementation" out-of-scope item still said "the multi-lens dependency-management substrate primitive remains Open Q6" — same stale framing as the other 4 sites fixed in c7cc9f7. Reworded to "the LensAlgebra<F> + composed-lens-algebra substrate work is ratified by Q6 (NOT a separate primitive; derives from fold_node)." Final scan now shows no remaining stale "multi-lens substrate primitive" references that aren't in negation/disclaimer contexts. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address cursor APPROVE_WITH_COMMENTS — 3 partial-unification slips cursor/composer-2.5 caught three partial-unification slips: 1. Line 790 vs 792-799 — apply_diff classified as derived at 790, but Read/edit primitives table at 792-799 still listed it (+ subterm_at / apply_lens / affected_set) under a "Primitive" column with primitive- level semantics. Split authority inside same doc. FIX: section title changed to "Read/edit vocabulary (substrate types + derived combinators)". Each row now marked as either "carrier type" (Path, Edit, Diff — substrate-data types) or "derived combinator" (apply_diff, subterm_at, apply_lens, affected_set — fold_node instances). Note at section head explicitly says these are NOT new primitives per the main primitive set table. 2. Line 1240 (Ratified Q9) — said "the compiler must not trust its own search/fold", contradicting the T-9-ratified "find_witness is not a search" discipline. FIX: replaced "search/fold" with "candidate-enumeration" — consistent with the rest of the doc's T-9-aligned framing. 3. Line 1338 (glossary ClosedWorldDependencyWitness) — Pass B witness taxonomy collapsed this into StructuralPropertyWitness<P>, but the glossary still defined it as a standalone witness. Risks Worker A implementing the old carrier name. FIX: glossary entry now annotated "collapsed into StructuralPropertyWitness<P> per Pass B witness taxonomy — instance with P = being-completely-classified." Same pattern as solve_constraints / coercion fold / LawfulRewriteWitness derived- instance annotations elsewhere in the glossary. Net: all three internal-consistency issues resolved. apply_diff is consistently derived everywhere; "search" language consistently disclaimed per T-9; witness collapse consistently applied in glossary. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix apply_diff sequential semantics — substantive codex finding CRITICAL substantive finding from codex (sha b5d66eb): my apply_diff unification simplification was semantically WRONG. I had written apply_diff = fold_node(root, substitute_at_paths(diff)) — a single fold over the source with all paths substituted in parallel. But the read/edit pipeline doc requires SEQUENTIAL ordered semantics: - Each Edit applies to the current CANDIDATE state, not the original root. - Each subsequent Edit's Path resolves against the post-prior-Edit state. - Fail-closed if any Path doesn't resolve in the intermediate candidate. The "parallel substitution" framing would have lost the read/edit pipeline's per-Edit sequential resolution + fail-closed-on-intermediate- state semantics. P2/P3 violation. FIX: apply_diff reframed correctly across all 5 sites as: sequence_outcome(diff.edits, fn(edit, candidate) -> fold_node(candidate, substitute_at(edit.at, edit.replacement))) Composes fold_node + sequence_outcome (both derived combinators of fold_node). Each Edit applies to the *intermediate* candidate; sequential semantics preserved; fail-closed-on-unresolved-Path-in-intermediate-state preserved. 5 sites updated: - Line 104 (derived combinators in TL;DR) - Line 649 (derived combinators paragraph) - Line 790 (EDIT direction intro) - Line 801 (Read/edit vocabulary table) - Line 1347 (glossary entry) The unification still holds (apply_diff is derived from fold_node + sequence_outcome, not a separate primitive). The semantics are now correct: sequential per-Edit application, not parallel substitution. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: fix Q6 scheduling-authority split — lens-dep DAG is a P6 instance Codex correctly flagged that line 1224 created a second scheduling authority: "composed-lens-algebra construction (which is itself a fold_node over the lens-dependency DAG)" — a parallel ordering authority to the Typed dependency graph + topological/SCC machinery primitive (P6's own ordering authority). P2 single-authority violation: TWO sites would own topological ordering — the typed-dep-graph primitive AND the lens-construction-fold. FIX: clarify that the lens-dependency DAG IS a typed dependency graph instance (per P6 — kinds like LensReadsLensOutput / LensRequiresFact), and its topological order is computed by the SAME P6 primitive (Typed dependency graph + topological/SCC machinery) that produces all program-level orderings. Composed lens algebra construction CONSUMES the topological order from that primitive — single scheduling authority, NOT a separate fold over the lens-dep DAG. Single authority preserved. The lens-dependency DAG is one of the typed-dep-graph primitive's consumer surfaces, not a parallel ordering mechanism. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix substrate-home contradiction find_witness vs predicate algebras Codex (openai-pro?) flagged that lines 638 + 1136 contradicted on where the predicate algebras live: - Line 638: find_witness primitive in std/find_witness.dag; predicate algebras in their consuming concept-homes (std/constraints.dag + std/coercion.dag). - Line 1136: find_witness primitive in std/find_witness.dag; predicate algebras also in std/find_witness.dag (replacing the separate files). Duplicate substrate authority — P2 violation. FIX: line 1136 reworded to match line 638. The find_witness primitive is generic and lives in std/find_witness.dag; the predicate algebras live in their consuming concept-homes per M10 (concepts get proper homes): - constraint-satisfaction predicate in std/constraints.dag - exact-structural-equality-zip-fold predicate in std/coercion.dag Worker B authors all three files (primitive + two algebras). Single authority per concept; primitive in find_witness.dag, predicates in their respective consuming files. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address openai-pro REQUEST_CHANGES — apply_lens glossary + find_witness ambiguity contract Two findings from openai-pro (sha e5a841a): FINDING 1 — apply_lens glossary entry stale. Line 1348 still defined apply_lens as "the substrate-level read-side primitive lenses use" — contradicts the reclassification of apply_lens as a derived combinator at line 803 ("read/edit vocabulary is NOT primitives"). P2 parallel-authority violation. FIX: glossary entry updated to "(DERIVED, not primitive) ... Derived combinator post-Pass B unification — fold_node with the lens's algebra; combinator owns StageDiagnosticPolicy (per Q4). Composes with fold_node, doesn't extend the primitive set." Matches the derived classification at lines 803 + 1146. FINDING 2 — find_witness "first match" dilutes ambiguity contract. Line 638 said "first match returns Outcome::Accepted; multiple matches return AmbiguousTargetCandidate" — but "first match returns" is an execution instruction a worker could faithfully implement while SKIPPING ambiguity detection. That would silently accept positionally-first candidates, violating fail-closed and Q14's "deterministic policy OR fail-closed-ambiguity" semantics. FIX: find_witness contract rewritten to require collecting ALL passing candidates before any acceptance decision: - Enumerate the ENTIRE closed candidate set; check predicate against EVERY candidate; collect ALL passing candidates. - THEN resolve: * Exactly one passing ⇒ Accepted. * Zero passing ⇒ Rejected(NoTargetCandidate). * Multiple passing ⇒ apply declared TargetSelectionPolicy (Q14); deterministic policy → Accepted(selected); no policy OR policy fails to disambiguate → Rejected(AmbiguousTargetCandidate). - NO positional-first-wins. Ambiguity detection is required. Fail-closed semantics preserved per Q14 + P3. Workers cannot faithfully implement a positional-first variant and pass review; the contract demands full enumeration before acceptance. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: TL;DR find_witness — remove 'first match wins'; match line 638 contract One more 'first match' reference missed in the prior sweep: line 99 (TL;DR) still said 'first match wins (or fail-closed when zero, ambiguity diagnostic when multiple).' That's the same positional-first problem as line 638 (already fixed). FIX: TL;DR description now matches line 638: collects ALL passing candidates before resolving; ambiguity detection required; no positional-first-wins. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: reconcile find_witness result shape to ratified Outcome record form (codex finding) codex flagged that line 638's find_witness contract still used positional Outcome::Accepted(candidate, witness) / Outcome::Rejected(NoTargetCandidate) spellings, contradicting the ratified two-variant record shape at line 640 + line 1263 + TASKS.md line 424: Outcome<T> = Accepted { value: T, diagnostics } | Rejected { diagnostics: NonEmptyDiagnostics } Two incompatible result shapes in the same design brief = single-authority violation (P2 / Practice 5). Implementers get conflicting API instructions at the exact primitive this PR is redefining. FIX: line 638 reworded to use the record/struct form throughout: - Accepted { value: (candidate, witness), diagnostics } - Rejected { diagnostics: NonEmptyDiagnostics { head: NoTargetCandidate {...}, ... } } - Rejected { diagnostics: NonEmptyDiagnostics { head: AmbiguousTargetCandidate { candidates }, ... } } with explicit parenthetical 'record/struct shape per Ratified Q11 — NOT positional variant constructors' to anchor the convention. Matches the existing record-shape spelling at line 1286. Verified by grep: no other Outcome::X(...) positional constructions remain in docs/design-v4-compiler-homomorphism.md or src/v4/TASKS.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: parameterize find_witness with caller-supplied MultiplicityPolicy (openai-pro finding) openai-pro flagged a substrate-contract bug: the generic find_witness primitive at lines 99 + 638 specified 'multiple ⇒ apply TargetSelectionPolicy per Ratified Q14,' but Q14 is scoped to target COERCION ambiguity (target language declares the policy). The same find_witness primitive is also used by Ground/infer for solve_constraints, where the output is the canonical SOURCE grounding. Baking target-selection into the generic level would let a future worker faithfully implement 'apply TargetSelectionPolicy' in a source-grounding context where the contract should be 'canonical or diagnosed ambiguous' — silently accepting an ambiguous canonical grounding via target-model preference. P3 fail-closed violation + single-authority violation (modeling-discipline.md Practice 5). FIX: add MultiplicityPolicy as the 4th parameter to find_witness; caller supplies per use site. find_witness( source_facts, closed_candidate_set, preservation_predicate, multiplicity_policy: MultiplicityPolicy, // <-- new, caller-supplied ) -> Outcome<(Candidate, Witness)> MultiplicityPolicy = | UniqueOnly // exactly-one or fail-closed | TargetSelection(TargetSelectionPolicy) // Q14 — target coercion only | RewritePolicy(...) // P7 placeholder solve_constraints binds MultiplicityPolicy::UniqueOnly unconditionally (canonical source grounding — no target-preference notion) coercion fold binds MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) (Q14, target-coercion-specific) LawfulRewriteWitness will bind MultiplicityPolicy::RewritePolicy when P7 lands Updates touched (consistency sweep): - TL;DR (line 99) — primitive signature + caller-binding examples - Primitive table (line 638) — full contract with all three multiplicity cases - Derived combinators (lines 650-652) — each call site shows its policy binding - Substrate-home note (line 1136) — std/find_witness.dag carries MultiplicityPolicy type; per-caller policy bindings live in std/constraints.dag (UniqueOnly) and std/coercion.dag (TargetSelection) - Q14 ratification (line 1282) — explicit scope clarification: TargetSelectionPolicy goes inside MultiplicityPolicy::TargetSelection, supplied ONLY by the coercion fold call site; generic primitive does NOT bake it in - Glossary (line 1335) — signature updated to include multiplicity_policy Separates substrate-level multiplicity-policy authority (the MultiplicityPolicy type, lives with the find_witness primitive in std/find_witness.dag) from target-language-level target-selection authority (the TargetSelectionPolicy value, lives with each target LanguageModel). Two distinct authorities — neither collapsed into the other. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: fix fold_node landed-vs-planned algebra conflation (briansrls inline finding) briansrls flagged a P2 live-substrate/primitive-contract split at line 636: the design said the landed fold_node algebra is fn(R, Edge, Node) -> Outcome<R> (pure-success-accumulator) but src/v4/std/node.dag line 43 shows the actual landed NodeFold<R> as init: fn(Node) -> R step: fn(R, Edge, R) -> R (pure catamorphism — no Outcome) These are not the same shape. The landed step is a true catamorphism combiner: takes the accumulator, the edge, and the ALREADY-FOLDED child result R. The doc was describing the planned NodeOutcomeFold DERIVED combinator (Worker C escalated signature-collapse) as if it were already landed at the primitive level. This created two problems: 1. P2 boundary discipline — doc-claim contradicts on-disk substrate. 2. Implementers reading the design would write algebras that don't typecheck against the actual NodeFold<R> carrier. FIX (line 636 only): rewrite the primitive table entry to honestly separate landed-vs-planned: Landed primitive (NodeFold<R>): - init: fn(Node) -> R - step: fn(R, Edge, R) -> R -- pure catamorphism, no Outcome - lives in src/v4/std/node.dag line 43 Planned derived combinator (NodeOutcomeFold): - algebra: fn(R, Edge, Node) -> Outcome<R> -- pure-success-accumulator - combinator interprets StageDiagnosticPolicy - lives at the derived-combinator layer (Worker C scope) - lands as part of the 43-callsite Outcome-shape migration Outcome-threading is explicitly stated as NOT in the primitive — it lives in the derived NodeOutcomeFold combinator. This preserves the single-authority discipline (combinator owns failure policy) while honestly reporting the on-disk shape. Verified lines 103, 648, 1183 (TL;DR + derived-combinators + Ratified Q4) all describe the DERIVED NodeOutcomeFold combinator, not the landed primitive — they're correctly contextualized in their respective sections. Only line 636 conflated the two. Cross-checked: src/v4/std/node.dag lines 43-46 confirm landed shape. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address cursor APPROVE_WITH_COMMENTS — bootstrap-table + 3 staleness syncs cursor BLOCKING (lines 528-529): the bootstrap substrate table listed BootstrapWitness + FixedPointWitness as separate concepts to declare, directly below line 511's witness taxonomy collapse that explicitly folds both into PromotionWitness. Parallel authority in the same section (P2 / Practice 5). FIX (line 528, single row replaces two): PromotionWitness (composed gate; Pass B witness-taxonomy unification) - sub-field (a): bootstrap-roundtrip check — Stage0Candidate[k+1] produces Stage1Candidate[k+1] (was BootstrapWitness) - sub-field (b): fixed-point check — Stage1[k] compiles to itself (was FixedPointWitness) Internal sub-fields, not separate authorities; matches line 511. cursor exploratory observations (3 staleness syncs to keep the doc internally coherent post-Pass-B): 1. Line 523 — Stage0Contract description said 'fold_node + traverse'; updated to 'fold_node + derived traverse_node combinator' to match Pass B's derived-combinator framing. 2. Lines 478-480 (Layer 1 substrate stack) — listed traverse + coercion fold as substrate primitives. Updated to the post-Pass-B 5-primitive set (Node, fold_node, find_witness, Outcome/Diagnostic/Locus, grammar-as-data, typed dependency graph, change/artifact/bootstrap substrate) + an explicit 'derived combinators on top' line listing traverse_node / sequence_node / bind_outcome / apply_diff / coercion fold / solve_constraints. 3. Line 1328 (Practice 10 glossary) — said 'use a substrate primitive (fold_node, traverse, coercion fold)'. Updated to distinguish primitives (fold_node, find_witness) from derived combinators (traverse_node, coercion fold, solve_constraints, etc.) — still directs implementers to those instead of hand-rolling. No new content; just resolves three places where the unification's collapsed primitive set hadn't propagated. Internal consistency restored against the 5-primitive table at line 632. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: unify PromotionWitness wording across bootstrap sections Co-authored-by: Brian Searls <briansrls@users.noreply.github.com> * design: trivial doc-hygiene per cursor exploratory observations (APPROVE) cursor APPROVE verdict on PR #3443 noted two non-blocking doc-hygiene exploratory observations. Trivial fixes since I'm here. 1. Line 1169 — Q0 ratification body said the new substrate question it raises is 'Open Q6 — multi-lens dependency management.' But Q6 IS ratified in this same PR (Ratified Q6 at line 1218). FIX: updated to 'Ratified Q6 — multi-lens execution derives from fold_node with a composed-lens-algebra' — matches the actual Q6 ratification title at line 1218. 2. Line 1274 (Q12 ratification body) said 'Already in the primitive set table (line 636).' But after Pass B edits, the table header is line 636 and Grammar-as-bidirectional-data row is at line 639. Brittle line-number reference. FIX: replaced the line number with a stable section-relative reference: 'see the Grammar-as-bidirectional-data row under The primitive set — the things the compiler IS.' Robust against future line drift. No semantic change; pure doc-hygiene reconcile. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: openai-pro REQUEST_CHANGES — 3 substrate-contract fixes openai-pro flagged three internally-inconsistent contracts on the current head (sha 8c1e199). All three would cause an implementer to encode the wrong primitive surface. Fixed: 1. NodeOutcomeFold.step signature contradicted landed NodeFold<R> (lines 103 + 1185) The derived combinator section said the Outcome-threading algebra is fn(R, Edge, Node) -> Outcome<R>, but the landed primitive at src/v4/std/node.dag:43 has step: fn(R, Edge, R) -> R. Third parameter is the already-folded child R, not the raw Node. The Outcome-threading derived algebra should match the primitive step shape with Outcome wrapping ONLY — not change the parameter list. Otherwise the derived combinator isn't really a fold_node instance. FIX: both lines 103 + 1185 now say fn(R, Edge, R) -> Outcome<R> with explicit cross-reference to the landed NodeFold<R>.step shape at std/node.dag:43. Single authority preserved. 2. Glossary derived-call signatures dropped multiplicity_policy (lines 1340-1342) The primitive signature at line 1339 (1 row above) requires multiplicity_policy: MultiplicityPolicy as the 4th arg — that's the whole point of the openai-pro single-authority finding already addressed in 9a97376. But the glossary entries for solve_constraints / coercion fold / LawfulRewriteWitness directly below showed 3-arg calls without policy. Implementers reading the glossary first would copy the wrong shape and reintroduce the policy-ambiguity the unification was supposed to remove. FIX: glossary rows now name the 4th arg explicitly with caller- correct policy binding: - solve_constraints: MultiplicityPolicy::UniqueOnly (NOT optional, NOT defaulted; pass at call site) - coercion fold: MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) (sourced from target model per Q14; sole legitimate target- selection-policy leakage site) - LawfulRewriteWitness: MultiplicityPolicy::RewritePolicy(...) (gated on P7; documents future shape only — NOT in MVP) 3. MVP carrier required RewritePolicy variant while P7 deferred (line 1138 vs line 1149 / line 654) Line 1138 said the MVP std/find_witness.dag carrier must include UniqueOnly | TargetSelection(TargetSelectionPolicy) | RewritePolicy(...) variants and 'Worker B authors all three.' But line 654 says RewritePolicy is introduced when P7 lands, and line 1149 puts P7 out of MVP scope. Untracked premature substrate surface — would land a RewritePolicy variant with no consumer in MVP. FIX: line 1138 now scopes MVP variants to UniqueOnly | TargetSelection(TargetSelectionPolicy) ONLY. RewritePolicy(...) is explicitly NOT in MVP — it lands together with P7 lawful-rewrite work per the P7 trigger. Worker B authors three files; RewritePolicy is added at P7, not MVP. Verified: zero remaining 'fn(R, Edge, Node) -> Outcome<R>' references in the doc; all find_witness call shapes in the glossary now name multiplicity_policy explicitly with the correct per-caller binding. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: PromotionWitness fixed-point check binds to CANDIDATE not Stage1[k] (briansrls inline BLOCKING) briansrls flagged a load-bearing THESIS-facet-2 / T-15 violation at line 531: PromotionWitness composed a k+1 bootstrap-roundtrip check with a fixed-point check over Stage1[k] (the OLD stage). That would let the promotion gate replace stage0 without ever proving the CANDIDATE is a self-emitting fixed point — Stage1[k]'s stability was already proven at the prior k-1 → k promotion, so re-checking it proves nothing about the new candidate. A non-self-emitting candidate could pass the gate and become Stage0[k+1]. THESIS facet 2 (compiler self-emits) would no longer hold by construction. FIX (3 sites): 1. Line 531 (bootstrap substrate table — the inline-flagged line): PromotionWitness composes (a) candidate-bootstrap-roundtrip — Stage0Candidate[k+1] produces Stage1Candidate[k+1] (b) candidate-fixed-point — Stage1Candidate[k+1] compiles to itself Both sub-checks now explicitly bound to the CANDIDATE at k+1, with an explicit warning that the fixed-point check is NOT over Stage1[k] and why (otherwise the gate could promote a non-self- emitting compiler). 2. Line 511 (witness taxonomy table): PromotionWitness 'What it asserts' clause now says "This CANDIDATE (Stage0Candidate[k+1] + Stage1Candidate[k+1]) is promotion-ready: the candidate Stage1 is a fixed-point AND the candidate Stage0 bootstrap-roundtrips to the candidate Stage1" — matches (1). 3. Line 419 (epoch loop diagram): The in-epoch stability invariant 'verify(Stage1[k] == Stage1'[k])' was incorrectly bound to PromotionWitness[k].fixed_point_sub_check. It's not — PromotionWitness[k] was bound at the prior k-1 → k promotion (over the candidate that BECAME Stage1[k]). The in-epoch verify is a steady-state stability re-confirmation, not a PromotionWitness production. Updated the diagram to: - Explicitly call the in-epoch line 'in-epoch stability invariant' with a NOTE explaining it's NOT a promotion-witness check. - Update the 'Upgrade k → k+1' verify block to show both sub-checks binding to PromotionWitness[k+1] over the CANDIDATE: Stage0Candidate[k+1] can produce Stage1Candidate[k+1] ──> PromotionWitness[k+1].candidate_bootstrap_roundtrip_sub_check Stage1Candidate[k+1] is a fixed-point (self-emits) ──> PromotionWitness[k+1].candidate_fixed_point_sub_check - Add explicit closing note: 'gate requires both sub-checks pass — non-self-emitting candidate CANNOT be promoted; THESIS facet 2 holds by construction.' The previous wording was a paste-up artifact from the BootstrapWitness + FixedPointWitness collapse: the old FixedPointWitness was steady- state stability, and when we composed both into PromotionWitness I didn't re-bind the fixed-point check to the candidate. briansrls caught it correctly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
T-8 closeout carrying forward #3420 (canonical_symbols accessor + wave-1 LM), #3363 (resolve-stage coproduct dissolution + compile anchors), and #3381 (bucket-C de-prose / wave-1 naming). Rebuilt on current
main; removes accidental git conflict markers (<<<<<<</=======/>>>>>>>) that caused v4 parse failures (expected 'module', found Lt).Test plan
src/v4/compiler/03_resolve.dag,dag.dag,resolve_compile_anchor.dagv2-compiler compile --source-root src/v4Carries: #3420, #3363, #3381