design: Pass A + Pass B amendments — strict simplification + primitive unification

[briansrls]

What this PR is

Strict-mode amendment to docs/design-v4-compiler-homomorphism.md + src/v4/TASKS.md per operator-direct architecture audit 2026-05-20. Follow-on to the merged PR #3437 (the original architecture doc) — addresses three categories of issues identified by audit and reviewer findings against the in-flight Wave-1 worker PRs (#3439/#3440/#3441).

What changed

Pass A — concrete violations (3 fixes)

1. Stripped Lossy from CoercionQuality lattice (P3 fail-closed violation). TASKS.md T-9 lines 419-420 amended: CoercionQuality = Identity | Exact only. Lossy operations are explicit user-declared source operations, not a coercion-time category. Loss is a diagnostic via CoercionMismatchKind, NOT a success-with-warning.
2. Stripped TranslatePlan.RewrittenThenCoerced extension slot (P2 illegal-states-unrepresentable — pre-emptive extension slot for unbuilt LawfulRewriteWitness was constructible).
3. Collapsed three named MVPs to one (P2 multiple-terminuses-for-one-boundary). MVP is compile(corenode, dag_lang, TranslateTo(rust_lang)) for the canonical add(x, y) = x + y worked example. Other endpoints (file-to-file shim, eval, multi-target translate) 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), 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 subsumes:

• solve_constraints (constraint-satisfaction predicate)
• The coercion fold (exact-structural-equality-zip-fold predicate)
• LawfulRewriteWitness (lawful-rewrite-precondition predicate, P7)

All three are find_witness invocations with different preservation predicates.

Derived (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)).

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 + LawfulRewriteWitness.
• PromotionWitness: was BootstrapWitness + FixedPointWitness.

Q6 + Q9 ratified as side-effects of unification:

• Q6 (multi-lens): derives from fold_node + composed-lens-algebra; no new primitive.
• Q9 (witness checking): derivation untrusted, witness check trusted; all 3 witness carriers support verify_witness re-check.

Net summary

Surface	Before	After
Substrate primitives	9	5
Witness types	7	3
Premises	10 (P0-P9)	10 unchanged
Open Qs	15	0 (7 ratified, 6 deferred-with-trigger, 2 absorbed into unification)

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-targeted).

What this means for in-flight Wave-1 work

Wave-1 worker PRs (#3439, #3440, #3441) are paused under swift-dove-578's coordination. Once this PR lands:

• Worker A (Wave-1 Worker A — std/dependency.dag + std/regeneration.dag + std/pipeline.dag (strict substrate) #3439) — targeted rework (DependencyEdge needs reason/subject; AcyclicityWitness + ClosedWorldDependencyWitness collapse to StructuralPropertyWitness

  ; NodeFileBinding absorption from Worker C).

• Worker B (Wave-1 Worker B — std/constraints.dag + std/coercion.dag (strict substrate, exact-only) #3440) — substantial rework or close-and-redispatch (solve_constraints + coercion fold merge into find_witness invocations; witness shape changes).
• Worker C (Wave-1 Worker C — infer lens-import cleanup + std/outcome.dag traverse + extdeps/file_system.dag effects #3441) — biggest rework; close-and-redispatch likely cleanest (traverse_node becomes derived from fold_node; 43-callsite Outcome migration cascade; multiple substrate findings already escalated by Worker C while paused).

The corrections-round dispatch shape is for swift-dove-578 to coordinate post-merge.

Constraints satisfied

References (per CLAUDE.md "Ledger standing principle" — single-authority):

• THESIS.md — The derived homomorphism; concept unification; fail-closed.
• INVARIANTS.md — P2 boundary discipline; P3 fail-closed; P5 progress-is-dissolution.
• docs/modeling-discipline.md — Practices 4, 8, 10.
• docs/design-read-edit-pipeline.md — read/edit pipeline composition (read/write-symmetric primitive layer).
• src/v4/TASKS.md — T-9 ratification (D2 reversal 2026-05-17 + Lossy strip 2026-05-20).

🤖 Generated with Claude Code

[briansrls]

Thanks for the APPROVE + the exploratory observation on dual-vocabulary watch.

On the "coercion fold" vs find_witness naming: the doc explicitly preserves "coercion fold" per the T-9 ratification (D2 reversal 2026-05-17 — "Name it the coercion fold; never an 'engine' or 'search algorithm'") while marking it conceptually as a find_witness invocation in the primitive set table and glossary. The dual-vocabulary is intentional and load-bearing for T-9 ratification continuity, not accidental.

The observation about downstream files is well-taken — worth watching that std/find_witness.dag (when authored, post-merge), std/coercion.dag, and std/constraints.dag don't drift into parallel-authority shapes. Worker corrections round under swift-dove-578 (post-merge of this PR) will be the test of whether the dual-vocabulary stays cleanly compatible or causes confusion in implementation. If it does cause confusion, that's a follow-on amendment, not a blocker on this PR.

No code change required from this review.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 45e8a3fb · Trigger: schedule
• Thinking: 195s wall

---

BLOCKING (1)

Root Cause

• docs/design-v4-compiler-homomorphism.md 635|Pass B primitive collapse was applied to the TL;DR/primitive table/glossary without reconciling P5/P7/Q4/MVP dispatch entries → update all authoritative sections to one primitive/dependent-combinator plan.

⚠️ The primitive unification is directionally coherent, but the doc must present one dispatchable primitive model before it drives implementation.

[briansrls]

Valid finding against sha 45e8a3f, addressed in commit 264cd2b.

Pass B primitive collapse now reconciled across all authoritative sections — single primitive plan, no split authorities:

• Q4 (line 1179) — now marks 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.
• P5 (line 296) — Practical implications rewritten so solve_constraints / coercion fold / LawfulRewriteWitness are all find_witness invocations with different preservation predicates.
• P7 (line 600) — Pipeline diagram + carrier description reframed to use find_witness with lawful-rewrite-precondition predicate.
• MVP dispatch entries — W-CoercionFold + W-TraverseOutcome are no longer separate primitive-implementation work items; reframed as find_witness / fold_node invocations with specific algebras-as-data.

One primitive plan, dispatchable. P2 single-authority boundary preserved.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 45e8a3fb · Trigger: manual
• Comparison: main @ deda6f21 ... session/smart-boar-330-design-unification @ 45e8a3fb
• Conversation: View conversation

---

1. Story of the diff

This PR is a design/planning amendment, not an implementation patch. It tightens docs/design-v4-compiler-homomorphism.md around the “strict simplification + primitive unification” story: the compiler primitive surface is collapsed to fold_node plus four non-fold primitives, with traverse_node / bind_outcome, apply_diff, solve_constraints, the coercion fold, and lawful rewrites reframed as derived uses of fold_node or find_witness (docs/design-v4-compiler-homomorphism.md:96-105, docs/design-v4-compiler-homomorphism.md:641-649, docs/design-v4-compiler-homomorphism.md:1327-1330). It also adds a witness-taxonomy collapse from seven named witnesses into three generic carriers (docs/design-v4-compiler-homomorphism.md:502-514) and narrows the MVP to one compile-core endpoint, CoreNode -> TargetSource for Rust, with shims/eval/multi-target/bootstrap promotion explicitly out of scope (docs/design-v4-compiler-homomorphism.md:1123-1146).

src/v4/TASKS.md is amended to align the native .dag language model’s canonical-symbol authority and to simplify coercion quality by removing Lossy, making lossy conversions explicit source operations rather than coercion-time successes (src/v4/TASKS.md:402-420). The intended mechanism is good: fewer primitives, fewer named witness variants, and fewer success-with-warning shapes. The problem is that a few planning lines still preserve the old carrier and primitive vocabulary, so the PR leaves multiple active authorities for the same substrate concepts.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Finding — Outcome<T> has conflicting substrate shapes in the same PR.

src/v4/TASKS.md:419 says a successful coercion is Outcome::Produced and failure is Outcome::Rejected { diagnostic: CoercionMismatchKind }. But this same PR ratifies the canonical shape as Accepted { value: T, diagnostics: Diagnostics } | Rejected { diagnostics: NonEmptyDiagnostics } and explicitly says “No Produced vs Accepted split” at docs/design-v4-compiler-homomorphism.md:1255-1260. The design doc also keeps the old singular-diagnostic shape in Q8 and Q14 at docs/design-v4-compiler-homomorphism.md:1226 and docs/design-v4-compiler-homomorphism.md:1278. This touches substrate, not implementation detail: Outcome<T> is the fail-closed carrier downstream stages will construct and consume. Boundary discipline requires each fact to live in exactly one authoritative place, and a boundary is not landed by a declaration alone when consumers could follow another active shape. chatgpt-review-30353853-29d6-48…

Fix: make every changed planning line use the Q11 shape: successful coercion is Outcome::Accepted { value: ..., diagnostics: ... } plus a separate quality tag; coercion mismatch is carried inside Rejected { diagnostics: NonEmptyDiagnostics }, not as a direct diagnostic field and not via Produced.

1. INVARIANTS.md + modeling-discipline.md. Finding — the multi-lens primitive is both dissolved and deferred.

The PR’s own unification says derived combinators are not primitives (docs/design-v4-compiler-homomorphism.md:641-649), and Q6 is resolved as fold_node(InferredTree, composed_lens_algebra) with “No new substrate primitive” (docs/design-v4-compiler-homomorphism.md:1208-1218). Yet the MVP out-of-scope list still defers a “Multi-lens dependency primitive (Open Q6)” at docs/design-v4-compiler-homomorphism.md:1143. That line preserves the old Open-Q primitive framing after the PR has ratified the dissolution. This violates Progress Is Dissolution: a scaffold or deferred surface must have a real dissolution target, not point workers at a concept the same PR says must not exist. chatgpt-review-30353853-29d6-48…

Fix: replace that item with the actual remaining work from docs/design-v4-compiler-homomorphism.md:1218: land LensAlgebra<F> and the composed-lens-algebra construction, not a “multi-lens dependency primitive.”

1. CODING.md. Compliant.

No Rust code or Rust comments are changed. The added prose is load-bearing design/planning text rather than explanatory commentary around implementation control flow, so CODING.md’s data+free-functions, small-function, and Rust comment-discipline rules are not the active failure mode here.

1. TESTING.md. N/A — docs/planning-only diff.

The diff does not add executable compiler behavior, runner behavior, or a new test harness. The merge blockers are contradictory substrate/planning authorities, not missing regression coverage. Under the current 0-floor trajectory, new boundary/test intent should eventually default to .dag TestClaim where applicable, but this PR does not introduce such a runnable behavior surface. chatgpt-review-d16d77b8-d1db-41…

1. LOCKED DESIGN DECISIONS. Finding — the PR adds a reference to a retired DECISIONS ledger.

src/v4/TASKS.md:404 rewrites the CP-1b note to cite DECISIONS §CP-1b item 2. But the live modeling discipline explicitly says src/v4/DECISIONS.md is deleted and facts should not be re-listed in ledger docs; non-comment receipts are PR review, INVARIANTS.md §P5(b), src/v4/TASKS.md, and grounding receipts, not a resurrected DECISIONS authority. chatgpt-review-44c9f83d-4fa6-4e…

The same file later reiterates that older DECISIONS.md references are only tolerated as historical text unless the sentence is rewritten; this sentence is rewritten in this PR. chatgpt-review-44c9f83d-4fa6-4e…

Fix: cite the live authority directly, likely src/v4/TASKS.md’s CP-1b/T-8 row or the relevant PR-review/commit receipt, not DECISIONS.

1. TRACKED vs UNTRACKED DEBT. Finding — an Outcome reconcile is left as an unbounded scaffold while stale Outcome shapes remain active.

docs/design-v4-compiler-homomorphism.md:637 says the Diagnostic + Locus carrier “needs Outcome-shape reconcile in corrections round,” but the same PR keeps the old Produced and singular diagnostic shapes at src/v4/TASKS.md:419, docs/design-v4-compiler-homomorphism.md:1226, and docs/design-v4-compiler-homomorphism.md:1278. “Corrections round” is not a bounded dissolution trigger with an owner/task; it is a vague future bucket. Since the conflicting shape is substrate-level and newly preserved by this PR, this should be resolved in this PR rather than carried as informal debt.

2.5. Top-down PM intent review

Finding — one MVP line would cause a worker to execute the opposite of the primitive-unification plan.

The highest-level intent of this PR is strict primitive simplification: it says the full compiler primitive surface is five things at docs/design-v4-compiler-homomorphism.md:639, and it ratifies Q6 as fold_node with a composed lens algebra, with “No new substrate primitive” at docs/design-v4-compiler-homomorphism.md:1208-1218. But docs/design-v4-compiler-homomorphism.md:1143 still instructs follow-on work as “Multi-lens dependency primitive (Open Q6)”. A worker following the MVP/out-of-scope list faithfully would go look for or design a primitive the ratified section explicitly removed. That dilutes the PM intent from “strict simplification + primitive unification” into “defer the old primitive.”

3. Verdict

REQUEST_CHANGES. The direction is strong, but the PR leaves contradictory active authorities for Outcome<T>, preserves a dissolved multi-lens primitive as future work, and adds a reference to a retired DECISIONS ledger. Because these are substrate/planning authorities, merging them would misdirect the implementation work this design is supposed to constrain.

[briansrls]

@codex finding addressed in commit 264cd2b0b. Pass B primitive collapse now reconciled across P5 / P7 / Q4 / MVP dispatch entries — single primitive plan, not split authorities:

• 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 (Lawful rewrites) — pipeline diagram + carrier description reframed to use find_witness with lawful-rewrite-precondition predicate. HomomorphismWitness<R> with different R values across exact-equality vs lawful-rewrite. Historical naming preserved per T-9 ratification.
• Q4 (traverse_node) — now explicitly marks 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 and W-TraverseOutcome reframed as find_witness / fold_node invocations with specific algebras-as-data, not separate primitive-implementation work items.

One primitive plan, dispatchable. No split authority.

— sent from smart-boar-330

[briansrls]

@openai-pro REQUEST_CHANGES addressed in commits 2023788f0 (TASKS.md) + 264cd2b0b (architecture doc). All four findings + the PM-intent issue resolved:

1. Outcome conflicting shapes — three sites updated to ratified Q11 two-variant shape:

• TASKS.md:419-420 — coercion quality tag + composition rule both reworded. Now: Outcome::Accepted { value, diagnostics: Diagnostics } for success, Outcome::Rejected { diagnostics: NonEmptyDiagnostics } for failure (with CoercionMismatchKind carried as diagnostic payload, not a direct field).
• docs/design-v4-compiler-homomorphism.md:1226 (Q8 ratification) — same.
• docs/design-v4-compiler-homomorphism.md:1278 (Q14 ratification) — same.

2. Multi-lens primitive dissolved-AND-deferred contradiction — MVP out-of-scope line replaced. Was "Multi-lens dependency primitive (Open Q6)" which contradicted 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; no resurrected DECISIONS ledger).

4. Outcome reconcile as bounded scope — 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 "corrections round" debt.

5. PM intent — the "Multi-lens dependency primitive" instruction that would have misdirected a worker is replaced with the actual substrate work (LensAlgebra + composed-lens-algebra construction).

Net: single substrate authority for Outcome; dissolved primitives stay dissolved (no zombie deferred references); citations route to live authorities; bounded scope for migration work.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 264cd2b0 · Trigger: manual
• Comparison: main @ deda6f21 ... session/smart-boar-330-design-unification @ 264cd2b0
• Conversation: View conversation

---

1. Story of the diff

This PR is a design/planning amendment that tightens the v4 compiler-core plan around a smaller primitive set. docs/design-v4-compiler-homomorphism.md collapses the earlier primitive list into fold_node plus four non-fold primitives, with find_witness absorbing the old solve_constraints, coercion-fold, and future lawful-rewrite witness shapes (docs/design-v4-compiler-homomorphism.md:96, :99, :642). It also narrows the MVP from three possible endpoints to one core homomorphism endpoint: CoreNode to Rust TargetSource, deferring eval, file shims, multi-target support, lawful rewrites, multi-lens scheduling, and bootstrap promotion behind named triggers (docs/design-v4-compiler-homomorphism.md:1126, :1130, :1141-1147). src/v4/TASKS.md aligns T-9 with the same strictness by removing Lossy from successful coercion quality and making information loss a rejected coercion with CoercionMismatchKind::WouldLoseInformation (src/v4/TASKS.md:420-421).

2. Invariant categories

1. LAYER MODEL — Finding. docs/design-v4-compiler-homomorphism.md:1187 says StageDiagnosticPolicy has a single authority in std/diagnostic.dag and is “NOT split across std/pipeline.dag,” but docs/design-v4-compiler-homomorphism.md:1259 says the same policy is “declared per stage in std/pipeline.dag.” This is substrate-level boundary design, and P2 requires every fact to live in exactly one authoritative place; as written, an implementer can reasonably author the policy carrier in both diagnostic and pipeline surfaces. If the intent is “the type lives in std/diagnostic.dag; stage rows in std/pipeline.dag merely reference values of that type,” say that explicitly and remove the split wording. chatgpt-review-e7f7e69a-0b48-4b…
2. INVARIANTS.md + modeling-discipline.md — Finding. docs/design-v4-compiler-homomorphism.md:1185 explicitly forbids map_node_outcome as a duplicate because map_node_outcome ≡ bind_outcome, but docs/design-v4-compiler-homomorphism.md:1266 reintroduces map_node_outcome as one of the combinators that threads StageDiagnosticPolicy. That violates the “don’t hand-roll a derived operation” / traverse-dissolution discipline: the design first names the duplicate helper as forbidden, then tells Worker C to wire it anyway. Replace the Q11 line with the canonical set from Q4, or explain why map_node_outcome is a distinct terminal combinator and give it a disposition. chatgpt-review-d7d3dba0-02af-47…
3. CODING.md — N/A. The diff is design/TASKS prose only; no Rust implementation, helper extraction, method shape, result type, or code-comment discipline is changed.
4. TESTING.md — N/A. No executable compiler behavior or test harness changes are introduced in this diff. For a design-only amendment, the relevant bar is whether the plan preserves the .dag/generated-test trajectory; it does not add Rust tests or remove test coverage.
5. LOCKED DESIGN DECISIONS — Compliant, aside from the two authority contradictions above. The PR makes its design changes explicit as rescopes/ratifications rather than silent drift: the MVP is marked as a strict 2026-05-20 rescope (docs/design-v4-compiler-homomorphism.md:1128), Q4 is updated as a derived traverse_node decision (docs/design-v4-compiler-homomorphism.md:1179-1188), and T-9’s coercion quality change is explicitly marked operator-direct (src/v4/TASKS.md:420). The remaining issue is not an unacknowledged locked-design divergence; it is internal inconsistency in the amended locked text.
6. TRACKED vs UNTRACKED DEBT — Compliant. The newly deferred MVP items each carry a dissolution/arrival trigger (docs/design-v4-compiler-homomorphism.md:1141-1147), and the Outcome migration is bounded as one Worker C corrections-packet task with a concrete 43-callsite scope (docs/design-v4-compiler-homomorphism.md:640, :1138). I did not see a new TODO/scaffold without bounds and trigger.

2.5. Top-down PM intent review

Compliant. The highest-level intent is the derived homomorphism: target facts are modeled locally and translation is derived by comparing groundings, with unfaithful translations surfaced as diagnostics rather than adapter code. chatgpt-review-bcd3f5fb-4eb8-48…

The PR preserves that intent by making the MVP a single homomorphism demonstration (docs/design-v4-compiler-homomorphism.md:1130, :1149), by stripping lossy coercion out of successful translation (src/v4/TASKS.md:420), and by pushing previously separate mechanisms into fold_node/find_witness rather than adding handwritten compiler paths (docs/design-v4-compiler-homomorphism.md:642-651). The two findings above need correction because they would cause worker-level substrate authority drift, but I do not see a PM-level semantic dilution of the plan.

3. Verdict

REQUEST_CHANGES. The overall simplification is directionally right, but the amended substrate plan currently contradicts itself on the StageDiagnosticPolicy authority and reintroduces a helper it explicitly forbids. Those are substrate-level planning defects; landing them would send implementation workers toward parallel authority.

[briansrls]

@codex finding addressed in commits af23c60e8 + a729d5689. The "search" descriptor that contradicted T-9 ratification has been stripped from all three sites where find_witness is described:

• Line 99 (TL;DR) — was "the search-structure-preserving primitive"; now "the unified candidate-enumeration-and-check primitive" with explicit "NOT a search, per src/v4/TASKS.md T-9 ratification" disclaimer.
• Line 638 (primitive set table) — was "THE structure-preservation-search primitive"; now "THE unified candidate-enumeration-and-check primitive" with the same NOT-a-search disclaimer + explicit framing as "mechanically enumerates the candidate set and checks the preservation predicate."
• Line ~1334 (glossary) — same swap.

The word "find" in find_witness is preserved (it denotes the operation's OUTPUT — a canonical candidate or a diagnostic — not a search algorithm). All three previously-distinct primitives (solve_constraints, coercion fold, LawfulRewriteWitness) remain unified under find_witness, but the mechanic is now explicitly framed as closed candidate enumeration + mechanical decidable-by-construction predicate check, consistent with T-9's "not a search, not research" rule.

Other uses of "search" in the doc (e.g., "not heuristic search", "never call it 'search'") are deliberate disclaimers / negations and are correct as-is.

Final sweep verified: no "structure-preservation-search" or "search-structure-preserving" descriptors remain on find_witness anywhere.

— sent from smart-boar-330

[briansrls]

@openai-pro both findings addressed in commit 26aa13cc0:

Finding 1 — StageDiagnosticPolicy authority contradiction (lines 1187 ↔ 1259).

The two passages did contradict each other as stated. Fixed by clarifying the type-vs-value distinction:

• The TYPE declaration type StageDiagnosticPolicy { accumulation: Accumulate | ShortCircuit; fatality: FailClosed (invariant) } lives in std/diagnostic.dag — single authority, extension of the existing Outcome substrate.
• 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 — that is not split authority, just the type-vs-value distinction.

Both Q4 line 1187 and Q11 line 1259 updated consistently.

Finding 2 — map_node_outcome reintroduced after being forbidden (lines 1185 ↔ 1266).

Q11 had reintroduced map_node_outcome in the combinator list, contradicting Q4's explicit "forbidden as duplicate of bind_outcome." Fixed by aligning Q11's list with Q4's canonical set:

• Canonical set: traverse_node / sequence_node / bind_outcome (per Ratified Q4).
• map_node_outcome explicitly forbidden in BOTH passages — use bind_outcome instead (per Worker C finding . #3, map_node_outcome ≡ bind_outcome).

Verified: map_node_outcome now only appears in the doc as the forbidden-duplicate disposition; no reintroduction anywhere.

Both fixes are internal-consistency cleanups; no architectural change. The substrate plan reads as one coherent design across Q4 + Q11.

— sent from smart-boar-330

[briansrls]

@codex finding addressed in commit 81a83a890. Valid P5 / Practice 9 finding — I had inadvertently 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=1.
• dsl/gunbc/ci_github_actions_workflow.dag references it.

Deleting the dissolution record without dissolving the scaffold is exactly the P5 violation the rule exists to prevent (yellow must dissolve, not just be untracked).

Fix: the bridge note has been restored verbatim from main. Both the CP-1b bucket C note (my intended edit) and the CI emit-wall bridge note (which I should not have deleted) now appear in T-8's planning surface. The dissolution trigger is unchanged: "typed resolve-only compiler gate lands OR emit reaches compiled: on standard-8 without host SIGTERM."

The deletion was inadvertent — inherited from session branch state when I created the new branch via git checkout session/smart-boar-330 -- src/v4/TASKS.md. 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.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 81a83a89 · Trigger: schedule
• Thinking: 171s wall

---

BLOCKING (1)

Root Cause

• docs/design-v4-compiler-homomorphism.md Pass B primitive collapse updated the TL;DR/table/Q6 sections but not the P3/P8/read-edit/testgen/self-edit references → reconcile every authoritative reference to apply_diff and multi-lens execution with the derived-combinator/composed-algebra model.

⚠️ The prior primitive-unification issue is mostly fixed, but the document still has a remaining single-authority conflict around the primitive boundary.

[briansrls]

Valid finding — addressed in commits c7cc9f7 + b5d66eb.

Five sites had stale framings that contradicted the "5 primitives total" claim from the primitive set table. All five updated to reference the unification consistently:

Q6 / multi-lens stale framings (5 sites):

• Line 256 (P3 commitment 5) — now: "See Ratified Q6 below — derives from fold_node + composed-lens-algebra; NO new substrate primitive."
• Line 267 (held-pending list) — now: "LensAlgebra + composed-lens-algebra construction (per Ratified Q6 — NOT a substrate primitive; derives from fold_node)."
• Line 598 (regen substrate impl order) — same reframe.
• Line 904 (testgen lens-to-lens deps) — same reframe.
• Line 1155 (lens framework out-of-scope) — same reframe.

apply_diff stale framings (3 sites):

• Line 790 (EDIT direction intro) — now: "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) — read/write-symmetric phrasing reworded as mechanism (fold_node reads; fold_node-with-substitute_at_paths writes) not primitive set.
• Line 1345 (glossary) — now: "(DERIVED, not primitive) The structural-edit derived combinator = fold_node(root, substitute_at_paths(diff))."

P2 single-authority preserved: implementers cannot read the doc and conclude that multi-lens execution or apply_diff is a separate primitive. The 5-primitive surface holds; everything else is derived.

— sent from smart-boar-330

[briansrls]

@cursor/composer-2.5 all three findings addressed in commit e90bdff89:

Finding 1 — apply_diff in Read/edit primitives table contradicts line 790.

The table at 792-799 was titled "### Read/edit primitives" with apply_diff (+ subterm_at / apply_lens / affected_set) under a "Primitive" column with primitive-level semantics. Fixed:

• Section renamed 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 with specific algebras).
• Note at section head explicitly states these are NOT new primitives; primitive set is per the main table above (5 primitives total).

Finding 2 — Q9 "search/fold" wording slip.

Line 1240 said "the compiler must not trust its own search/fold" — used "search" which contradicts the T-9 ratified "find_witness is not a search" discipline. Fixed: "search/fold" → "candidate-enumeration". Wording now consistent with the rest of the doc's T-9-aligned framing.

Finding 3 — ClosedWorldDependencyWitness glossary not collapsed.

Glossary entry at 1338 still defined ClosedWorldDependencyWitness as a standalone substrate witness while Pass B witness taxonomy (lines 503-515) collapsed it into StructuralPropertyWitness<P>. Fixed: glossary entry now annotated "(collapsed into StructuralPropertyWitness<P> per Pass B witness taxonomy — instance with P = being-completely-classified)" — same DERIVED-instance annotation pattern as solve_constraints / coercion fold / LawfulRewriteWitness elsewhere in the glossary.

Net: all three internal-consistency issues resolved.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e90bdff8 · Trigger: schedule
• Thinking: 216s wall

---

BLOCKING (2)

Root Cause

• docs/design-v4-compiler-homomorphism.md Pass B primitive collapse conflates "derived" with "single Node catamorphism" → define apply_diff as a derived ordered fold over Diff.edits using per-edit substitution/path diagnostics, or keep the existing operation primitive until that derivation is modeled.
• docs/design-v4-compiler-homomorphism.md Q6 collapses tree traversal and dependency scheduling into one fold_node story → split the design so the typed dependency graph orders lens dependencies and fold_node only performs the coalesced InferredTree traversal.

⚠️ Two primitive-collapse details still change semantics or duplicate an existing primitive boundary.

[briansrls]

Valid substantive finding — addressed in commits fddec66f8 + 4ef11ff08.

The single-fold framing was semantically WRONG. The read/edit pipeline doc requires sequential per-Edit application against the intermediate candidate, with fail-closed on Path resolution in the intermediate state — NOT parallel substitution from the original root.

Fix applied at 6 sites:
apply_diff = sequence_outcome(diff.edits, fn(edit, candidate) -> fold_node(candidate, substitute_at(edit.at, edit.replacement)))

Sequential Outcome-bind-fold over the Diff's ordered Edits list. Each Edit applies to the intermediate candidate (post-prior-Edit state); each subsequent Edit's Path resolves against that intermediate, NOT the original root. Fail-closed if any Path doesn't resolve in the current candidate.

The unification still holds (apply_diff is DERIVED from fold_node + sequence_outcome, both of which are derived combinators or the primitive fold_node itself; no new primitive). The semantics are now correct.

Sites updated (TL;DR, derived combinators paragraph, EDIT direction intro, Read/edit vocabulary table, glossary, self-edit section).

— sent from smart-boar-330

[briansrls]

Valid finding — addressed in commit e5a841a6d.

The lens-dependency DAG creating its own "fold_node over the lens-dep DAG" was indeed a parallel scheduling authority to the P6 Typed-dependency-graph primitive.

Fix: clarify that the lens-dependency DAG IS a typed-dependency-graph instance (per P6 — kinds like LensReadsLensOutput / LensRequiresFact); its topological order is computed by the same Typed-dep-graph + topological/SCC primitive that produces all program-level orderings. The composed lens algebra consumes the topological order from that primitive at algebra-construction time, rather than computing it via a separate fold.

Single scheduling authority preserved: the typed-dep-graph primitive owns topological/SCC ordering for ALL dependency graphs — program-level, artifact-level, and lens-level. The lens-dependency DAG is a consumer surface, not a parallel ordering mechanism.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e5a841a6 · Trigger: schedule
• Thinking: 225s wall

---

BLOCKING (1)

Root Cause

• docs/design-v4-compiler-homomorphism.md primitive collapse chose find_witness as the generic operation but did not choose one authoritative home for each predicate algebra → state whether predicate algebras live with the generic primitive or in their consuming domain files, then make MVP and primitive-table text match

⚠️ One remaining P2 authority split should be fixed before this lands.

[briansrls]

Valid finding — addressed in commit fe201d44f.

Line 1136 contradicted line 638 on where the predicate algebras live. The correct framing per M10 (concepts get proper homes):

• find_witness primitive (generic) lives in std/find_witness.dag — operation signature + Outcome<(Candidate, Witness)> shape.
• Predicate algebras live in their consuming concept-homes:
  • constraint-satisfaction predicate in std/constraints.dag
  • exact-structural-equality-zip-fold predicate in std/coercion.dag

Line 1136 reworded to match line 638. Worker B authors all three files (primitive + two algebras); single authority per concept; no lumping of all three into find_witness.dag.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: e5a841a6 · Trigger: manual
• Comparison: main @ deda6f21 ... session/smart-boar-330-design-unification @ e5a841a6
• Conversation: View conversation

---

1. Story of the diff

This PR is a design-surface simplification of the v4 compiler plan. It collapses the earlier “fold_node plus eight operations” framing into a smaller primitive set: fold_node, grammar-as-bidirectional-data, find_witness, typed dependency graph, and diagnostic/locus/Outcome, while reclassifying traverse_node, sequence_node, bind_outcome, apply_diff, the coercion fold, solve_constraints, and LawfulRewriteWitness as derived combinations rather than primitives (docs/design-v4-compiler-homomorphism.md:96-105, docs/design-v4-compiler-homomorphism.md:636-652). The load-bearing new mechanism is find_witness: constraint solving, exact coercion/homomorphism checking, and future lawful rewrites all become closed candidate enumeration plus a mechanical predicate check, not “search” (docs/design-v4-compiler-homomorphism.md:638, docs/design-v4-compiler-homomorphism.md:1335-1338). The PR also narrows the MVP to one endpoint—CoreNode .dag to Rust TargetSource—and moves eval, file shims, multi-target translation, lawful rewrites, lens algebra, and bootstrap promotion into explicitly triggered follow-on scope (docs/design-v4-compiler-homomorphism.md:1128-1151). src/v4/TASKS.md is updated to keep the same simplification: canonical symbol authority is clarified, and coercion quality is tightened so Lossy is no longer a successful coercion quality; lossy conversion must be an explicit modeled operation, while coercion failure is Outcome::Rejected with a typed mismatch diagnostic (src/v4/TASKS.md:402-405, src/v4/TASKS.md:424-425).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — single substrate authority / primitive unification: docs/design-v4-compiler-homomorphism.md:1348 still defines apply_lens as “the substrate-level read-side primitive lenses use,” but this same PR explicitly reclassifies apply_lens as a derived combinator at docs/design-v4-compiler-homomorphism.md:803 and says the read/edit vocabulary is “NOT primitives” at docs/design-v4-compiler-homomorphism.md:794. This line is outside the immediate added line, but it is PR-relevant because the PR edits the same glossary hunk at docs/design-v4-compiler-homomorphism.md:1347 to demote apply_diff; leaving the adjacent apply_lens primitive wording creates a parallel primitive-set authority. P2’s boundary rule is that every fact lives in exactly one authoritative place; here the primitive status of apply_lens has two answers. chatgpt-review-44933b2a-2919-43…

1. INVARIANTS.md + modeling-discipline.md.

Finding — fail-closed ambiguity contract: docs/design-v4-compiler-homomorphism.md:638 says find_witness “checks the preservation predicate against each candidate; first match returns Outcome::Accepted,” then later in the same sentence says multiple matches return AmbiguousTargetCandidate unless a TargetSelectionPolicy resolves. Those two mechanics are not equivalent: an implementation that literally returns on first match cannot prove the “multiple matches” case and can silently accept an ambiguous target candidate. That violates fail-closed and single-authority selection: the Q14 contract at docs/design-v4-compiler-homomorphism.md:1284-1286 says multiple structurally valid candidates must be resolved by declared target policy or rejected with AmbiguousTargetCandidate. The fix is to define find_witness as “collect/identify all passing candidates, apply declared selection policy if present, accept exactly the selected/unique candidate, otherwise reject.” P3 requires paths to succeed fully or fail with typed diagnostics, not accept a plausible first answer. chatgpt-review-44933b2a-2919-43…

1. CODING.md.

N/A — the diff is Markdown design/TASKS text only; it introduces no Rust functions, helpers, methods, error/result shapes, or comment-heavy implementation blocks governed by CODING.md.

1. TESTING.md.

N/A — this is a design-only amendment with no executable code path changed. I do not see a behavior implementation that would require a new Rust or .dag test in this PR; the long-term test direction remains .dag TestClaim / generated harnesses, with no Rust-side residual under the zero-floor target. chatgpt-review-225480ab-a6ad-41…

1. LOCKED DESIGN DECISIONS.

Compliant — the PR makes its design changes explicit as Pass B / Ratified Q6 / Q11 / Q12 / Q14 amendments rather than silently changing the plan. The MVP narrowing is framed as a first proof point and does not retract Pure Bootstrap to Zero or self-hosting; deferred items such as bootstrap promotion and stage0 candidate generation are still named follow-ons rather than deleted from the program.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the new MVP out-of-scope list carries explicit defer triggers for eval, file-to-file shim, multi-target translation, lawful rewrites, composed lens algebra, and bootstrap promotion (docs/design-v4-compiler-homomorphism.md:1143-1149). The Outcome-shape migration is also bounded as a single corrections-packet substrate task with a concrete scope of 43 callsites and one substrate authority (docs/design-v4-compiler-homomorphism.md:640). That matches P5’s scaffold discipline: named bridge, bounds, and dissolution trigger. chatgpt-review-44933b2a-2919-43…

2.5. Top-down PM intent review

Finding — the intended ambiguity semantics are diluted in the primitive definition. The PM-level intent of this PR is strict simplification without weakening fail-closed homomorphism selection: Q14 says multiple valid target candidates are resolved only by a declared TargetSelectionPolicy, otherwise the result is Outcome::Rejected with AmbiguousTargetCandidate (docs/design-v4-compiler-homomorphism.md:1284-1286). But the primitive table at docs/design-v4-compiler-homomorphism.md:638 says “first match returns Outcome::Accepted,” which is an execution instruction a worker could faithfully implement while skipping ambiguity detection. That changes the meaning of the plan from “deterministic or fail-closed” to “positional first-valid candidate may win,” which is exactly the semantic softness this PR otherwise tries to remove.

3. Verdict

REQUEST_CHANGES

The direction is good: the primitive unification and MVP simplification mostly preserve the project’s modeling discipline. I would not merge until the primitive contract is made fail-closed for ambiguity and the stale apply_lens glossary row is reconciled with the new derived-combinator classification.

[briansrls]

@openai-pro substrate-contract finding addressed in commits 05af3f552 (WIP-snapshotter) + 9a973764a.

You were right — the generic find_witness primitive at lines 99 + 638 baked in TargetSelectionPolicy (which is Q14-scoped, target-coercion-specific) at the substrate level. Because the same primitive is also invoked by solve_constraints for canonical source grounding (line 300 / 651 / 1336), a future worker could faithfully apply target-selection in a source-grounding context, silently accepting an ambiguous canonical grounding via target-model preference. Substrate single-authority violation + P3 fail-closed risk.

Fix: add MultiplicityPolicy as the 4th parameter to find_witness; each caller binds its own policy at the call 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

Per-caller bindings (cannot be confused):

• solve_constraints (Ground/infer) binds MultiplicityPolicy::UniqueOnly unconditionally — canonical source grounding has no notion of target preference; multiple passing ⇒ ambiguous grounding ⇒ fail-closed, period.
• The coercion fold (translate) binds MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) per Q14.
• LawfulRewriteWitness (P7, when implemented) introduces MultiplicityPolicy::RewritePolicy(...).

Consistency sweep across the doc:

• TL;DR (line 99) — primitive signature + caller-binding summary
• Primitive table (line 638) — full contract with all three multiplicity cases spelled out using record-shape Outcome
• Derived combinators (lines 650-652) — each call site now shows its policy binding (TargetSelection / UniqueOnly / RewritePolicy)
• Substrate-home note (line 1136) — std/find_witness.dag carries the MultiplicityPolicy carrier; per-caller policy bindings live in std/constraints.dag (UniqueOnly) and std/coercion.dag (TargetSelection)
• Q14 ratification (lines 1282-1288) — explicit scope clarification block: TargetSelectionPolicy is the value that goes into MultiplicityPolicy::TargetSelection(...) supplied by the coercion fold call site ONLY; the generic primitive does NOT bake it in; non-target use sites cannot opt into target-selection
• Glossary (line 1335/1337) — signature updated to include multiplicity_policy: MultiplicityPolicy

Authority split (the PM-level intent you flagged): two distinct authorities, neither collapsed into the other —

1. Substrate-level multiplicity-policy authority = the MultiplicityPolicy type, lives with the find_witness primitive in std/find_witness.dag. Enumerates the legal kinds of multiplicity resolution.
2. Target-language-level target-selection authority = the TargetSelectionPolicy value, lives with each target LanguageModel (per Q14). The target picks its own preference.

MultiplicityPolicy::TargetSelection(...) is the bridge: it carries a TargetSelectionPolicy value into the primitive, but only when the coercion-fold call site supplies it. Source-grounding cannot route around it.

— sent from smart-boar-330

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9a973764 · Trigger: schedule
• Thinking: 170s wall

---

BLOCKING (1)

Root Cause

• docs/design-v4-compiler-homomorphism.md Primitive-collapse text moved Outcome traversal semantics onto the landed fold_node row → keep the pure landed NodeFold<R> contract separate from the future NodeOutcomeFold/traverse_node derived-combinator contract, or change the substrate in the same authority update.

⚠️ One primitive-contract inconsistency remains in the design doc.

[briansrls]

@briansrls inline BLOCKING at docs/design-v4-compiler-homomorphism.md:636 addressed in commit 896e0cbf5.

You were right — the doc claimed the landed fold_node algebra is fn(R, Edge, Node) -> Outcome<R> while src/v4/std/node.dag lines 43-46 actually carry:

type NodeFold<R> {
  init: fn(Node) -> R
  step: fn(R, Edge, R) -> R
}

— pure catamorphism, no Outcome, third step parameter is the already-folded child R not the raw Node. The doc was describing the planned NodeOutcomeFold derived combinator (Worker C escalated signature-collapse) as if it were the landed primitive. P2 live-substrate/primitive-contract split, exactly as flagged.

Fix (line 636 only): rewrote the primitive table entry to honestly separate landed-vs-planned:

• Landed NodeFold<R> carrier (pure catamorphism, no Outcome at the primitive level): init: fn(Node) -> R + step: fn(R, Edge, R) -> R — matches src/v4/std/node.dag:43 exactly.
• Outcome-threading is NOT in the primitive — it lives in the derived NodeOutcomeFold combinator at the derived-combinator layer, where the combinator (not the algebra) interprets StageDiagnosticPolicy. This combinator is not yet landed; Worker C delivers it as part of the 43-callsite Outcome-shape migration.

Separating the pure-catamorphism primitive from the Outcome-threading combinator is what keeps single-authority for failure handling at the combinator layer — same architectural intent as before, but now honestly reported.

Verified other references are correctly contextualized:

• Line 103 (TL;DR) — explicitly in the "primitives in earlier drafts but are now derived" section, describes NodeOutcomeFold algebra
• Line 648 (Derived combinators section) — explicit "derived" framing
• Line 1183 (Ratified Q4) — explicit "Worker C escalated NodeOutcomeFold.step signature collapse" framing

Only line 636 conflated landed primitive with planned derived combinator. Single-line edit fixes it.

Awaiting the +1 more queued comment.

[briansrls]

@codex finding addressed in commit 896e0cbf5 (one commit ahead of the 9a973764 sha you reviewed). Same finding briansrls flagged inline at line 636 at 18:22:57Z — these arrived in parallel after I had already pushed the fix; the relay is reading the pre-fix sha.

Fix at line 636 (verified on HEAD 896e0cbf5): primitive table entry now honestly separates landed NodeFold<R> from the planned NodeOutcomeFold derived combinator:

// LANDED in src/v4/std/node.dag line 43 — pure catamorphism, NO Outcome at primitive level:
type NodeFold<R> {
  init: fn(Node) -> R                  // seed per-Node
  step: fn(R, Edge, R) -> R            // combine accumulator + edge + already-folded child R
}

Outcome-threading is explicitly NOT in the primitive — the new line 636 text states "lives in the derived NodeOutcomeFold combinator (see Derived combinators below), where the combinator (not the algebra) interprets StageDiagnosticPolicy." Combinator is not yet landed; Worker C delivers it as part of the 43-callsite Outcome-shape migration.

Other doc references (lines 103 TL;DR, 648 Derived combinators, 1183 Ratified Q4) were already correctly contextualized in their respective sections — they describe the DERIVED NodeOutcomeFold, not the landed primitive. Line 636 was the sole conflation.

Single-authority restored: landed NodeFold<R> carrier matches src/v4/std/node.dag:43 exactly; planned NodeOutcomeFold lives in the derived-combinator layer with explicit "not yet landed" marker.

— sent from smart-boar-330

[briansrls]

@cursor BLOCKING + 3 exploratory observations addressed in commit 8b017fffc.

BLOCKING (lines 528-529) — bootstrap table parallel authority:

You were right — line 511 collapses BootstrapWitness + FixedPointWitness → PromotionWitness (composed gate) in the Pass B witness taxonomy, but the bootstrap substrate table directly below listed them as two separate concepts to declare. Implementers reading the bottom of the section would see three carriers instead of one composed gate.

Fix: collapsed lines 528-529 into a single PromotionWitness row that explicitly names the two sub-checks as internal sub-fields (not separate authorities):

PromotionWitness (composed gate; Pass B witness-taxonomy unification) | Single promotion-gate witness composing two specific checks: (a) the bootstrap-roundtrip check — Stage0Candidate[k+1] can produce Stage1Candidate[k+1] (was BootstrapWitness); (b) the fixed-point check — Stage1[k] compiles to itself (was FixedPointWitness). The two checks are internal sub-fields of the single PromotionWitness carrier — NOT separate authorities. Implementers see one promotion-ready witness, not three. Matches the witness-taxonomy collapse at line 511 above (no parallel authority).

Exploratory observation 1 (line 523) — Stage0Contract description:

Updated fold_node + traverse → fold_node + derived traverse_node combinator to match Pass B derived-combinator framing.

Exploratory observation 2 (lines 478-480) — Layer 1 substrate stack:

The old stack listed traverse + coercion fold as primitives. Updated to the post-Pass-B 5-primitive set:

• Node, fold_node, find_witness (unified Pass B primitive), Outcome/Diagnostic/Locus, grammar-as-data, typed dependency graph, change/artifact/bootstrap substrate

…plus an explicit "Derived combinators on top" line:

• traverse_node, sequence_node, bind_outcome, apply_diff, coercion fold, solve_constraints (all are fold_node / find_witness invocations, not primitives)

Exploratory observation 3 (line 1328) — Practice 10 glossary:

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. Per Pass B: traverse / coercion fold remain the right thing to reach for, just not the load-bearing label.

Internal consistency restored — the 5-primitive table at line 632 is now the single authority on the primitive set, and the Layer 1 stack + Practice 10 glossary + Stage0Contract row + bootstrap witness table all reference it coherently.

— sent from smart-boar-330

[cursor]

I focused on that 8b017fffc thread and validated the intended consistency points in docs/design-v4-compiler-homomorphism.md. The referenced fixes were present in the targeted sections (Layer 1 stack, Stage0Contract table row, PromotionWitness table row, Practice 10 glossary framing), but I found adjacent stale wording that still conflicted with the same single-authority intent.

I proactively fixed those residual inconsistencies in one follow-up commit (fbf6c1d91), specifically:

• Replaced bootstrap pipeline wording from BootstrapWitness + FixedPointWitness to the unified PromotionWitness composed-gate framing.
• Updated the epoch-loop check line to reference the fixed-point check as an internal PromotionWitness sub-check.
• Updated glossary Stage0Contract text to fold_node + derived traverse_node combinator.
• Replaced glossary BootstrapWitness / FixedPointWitness entry with a single PromotionWitness entry (with internal sub-fields).

Validation I ran:

• Targeted content checks with rg confirmed no remaining stale BootstrapWitness / FixedPointWitness pair entry or old fold_node + traverse glossary wording in those surfaces.
• Verified clean git state after commit/push.

  

[briansrls]

@cursor follow-up commit fbf6c1d91 verified and pulled into the working tree. All four edits are consistent with the Pass B unification direction and extend the consistency sweep I started in 8b017fffc:

1. Line 383 (three-pipelines table, bootstrap row) — BootstrapWitness + FixedPointWitness → PromotionWitness (composed gate with internal sub-checks). Live declaration reconciled.
2. Line 419 (epoch loop) — FixedPointWitness[k] → PromotionWitness[k].fixed_point_sub_check. Now references the composed-witness sub-field instead of the dissolved separate carrier.
3. Line 1371 (glossary Stage0Contract) — fold_node + traverse → fold_node + derived traverse_node combinator. Matches the post-Pass-B derived-combinator framing.
4. Line 1373 (glossary) — split BootstrapWitness / FixedPointWitness entry → single PromotionWitness entry with sub-field description. Glossary single-authority restored.

Residual scan (grep -n "BootstrapWitness\|FixedPointWitness" on the full file):

All remaining mentions are now strictly historical/explanatory — they explicitly call out the collapse:

• Line 514: "Was BootstrapWitness + FixedPointWitness — composed into one promotion-gate witness"
• Line 518: "BootstrapWitness + FixedPointWitness both gate promotion — one carrier composing the two specific checks" (the collapse rationale)
• Line 531: "(was BootstrapWitness)" / "(was FixedPointWitness)" (sub-field naming)
• Line 1375: "(formerly BootstrapWitness + FixedPointWitness)"

No live declarations remain. Internal consistency complete.

Carry-forward analysis (per review-gate-provenance discipline): fbf6c1d91 is doc-only, same-direction consistency clarification — no semantic change, no contract change. Prior approvals (claude + codex) carry forward. openai-pro re-review currently running on the new head will exercise the fresh state.

Thanks for the follow-up; saved a round-trip.

— sent from smart-boar-330

[cursor]

I re-validated that follow-up note directly against current HEAD, and it is accurate.

• The 4 cited edits are present exactly as described:
  • line 383: bootstrap row now uses PromotionWitness
  • line 419: epoch loop now references PromotionWitness[k].fixed_point_sub_check
  • line 1371: Stage0Contract now says fold_node + derived traverse_node combinator
  • line 1375 glossary row is a single PromotionWitness entry (with former pair noted historically)
• Residual mentions of BootstrapWitness / FixedPointWitness in docs/design-v4-compiler-homomorphism.md are explanatory/historical only, not live declarations.
• Cross-file check: no matches in src/v4/TASKS.md, and no other docs file under /workspace/docs contains those legacy names.

No additional patch was needed from this message; the consistency sweep is holding as intended.

  

[briansrls]

@cursor APPROVE noted, thanks. Both exploratory observations addressed in commit 8c1e199ca:

1. Line 1169 — Q0 ratification body said the new question it raises is "Open Q6 — multi-lens dependency management." Q6 is ratified in this same PR (line 1218). Updated to "Ratified Q6 — multi-lens execution derives from fold_node with a composed-lens-algebra" — matches the actual ratification title.

2. Line 1274 — Q12 ratification body said "Already in the primitive set table (line 636)." Brittle line-number reference (table header is at 636 but the Grammar row is at 639 after the Pass B edits). Replaced 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.

Pure doc-hygiene; no semantic change.

[cursor]

I checked that specific 8c1e199ca message against the latest branch state and confirmed it is now accurate on HEAD.

What I verified proactively:

• docs/design-v4-compiler-homomorphism.md:1169 now references Ratified Q6 (not “Open Q6”).
• docs/design-v4-compiler-homomorphism.md:1278 uses a stable section-relative pointer to the Grammar-as-bidirectional-data row, instead of a brittle hardcoded line reference.
• Branch head is currently 8c1e199ca, which is exactly the commit noted in the message.

I also handled branch drift while validating:

• Remote had advanced to include 8c1e199ca, so my local duplicate patch attempt was superseded.
• I rebased onto remote and skipped the duplicate commit cleanly.
• Current branch is clean and up to date; no further patch is needed for this message.

  

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 8c1e199c · Trigger: manual
• Comparison: main @ deda6f21 ... session/smart-boar-330-design-unification @ 8c1e199c
• Conversation: View conversation

---

1. Story of the diff

This PR is a design-level simplification pass over docs/design-v4-compiler-homomorphism.md, with a small matching amendment in src/v4/TASKS.md. It collapses the v4 compiler primitive set from a larger list into fold_node plus four other substrate operations, with find_witness becoming the unified candidate-enumeration-and-check primitive for constraint solving, target coercion, and future lawful rewrites. It also reclassifies traverse_node, sequence_node, bind_outcome, apply_diff, the coercion fold, solve_constraints, and LawfulRewriteWitness as derived combinators or named invocations rather than standalone primitives.

The load-bearing design move is that ambiguity and selection are no longer implicit: find_witness must collect all passing candidates and resolve multiplicity only through a caller-supplied MultiplicityPolicy. The PR then propagates that framing into lens scheduling, read/edit, bootstrap promotion witnesses, MVP scope, and TASKS T-9’s coercion-quality model, including stripping Lossy from successful coercions and making information loss a rejection diagnostic instead.

2. Invariant categories

1. LAYER MODEL — Finding

Finding — substrate derived-combinator contract is internally inconsistent. docs/design-v4-compiler-homomorphism.md:1185 says traverse_node is derived from fold_node, but gives the outcome-threading algebra as fn(R, Edge, Node) -> Outcome<R>. The same PR defines the landed NodeFold<R> primitive as step: fn(R, Edge, R) -> R, where the third parameter is the already-folded child result, not the raw child Node, at docs/design-v4-compiler-homomorphism.md:638.

That mismatch matters because this is substrate, not implementation prose: if NodeOutcomeFold.step sees Node instead of child result R, it is not a straightforward fold_node instance and either loses child-fold results or invites a second walker/substitution path. The fix should align the derived outcome combinator’s step shape with the primitive fold shape, likely fn(R, Edge, R) -> Outcome<R> unless the design explicitly names a different fold carrier and why it is still a fold-derived combinator.

2. INVARIANTS.md + modeling-discipline.md — Finding

Finding — API-level enforcement / single-authority: derived find_witness call signatures drop the required multiplicity policy. The PR’s canonical primitive signature requires multiplicity_policy: MultiplicityPolicy at docs/design-v4-compiler-homomorphism.md:1339, and the same line says the policy parameter is what keeps target-specific selection out of source-grounding contexts. But the glossary rows immediately below define solve_constraints, the coercion fold, and LawfulRewriteWitness as three-argument calls with no policy: docs/design-v4-compiler-homomorphism.md:1340, docs/design-v4-compiler-homomorphism.md:1341, and docs/design-v4-compiler-homomorphism.md:1342.

That recreates the ambiguity the PR is trying to remove. A worker following the glossary can implement an implicit default policy, a context-dependent policy, or a target-selection leak into source grounding. Those rows should name the fourth argument explicitly: MultiplicityPolicy::UniqueOnly for solve_constraints, MultiplicityPolicy::TargetSelection(target_lang.target_selection_policy) for target coercion, and a P7-gated rewrite policy only when lawful rewrites land.

3. CODING.md — N/A

N/A — this diff changes design documents and TASKS.md prose only; it does not add or refactor Rust implementation code, methods, helpers, error types, or comments in code files.

4. TESTING.md — N/A

N/A — this is a planning/design amendment with no executable code or test harness changes. The relevant risk is whether the design gives implementers a single correct contract, not whether a new runtime behavior needed a regression test in this PR.

5. LOCKED DESIGN DECISIONS — Compliant

The PR is explicit when it changes prior design status: Q4, Q6, Q7, Q8, Q9, Q11, Q12, and Q14 are marked ratified or deferred, apply_diff and LawfulRewriteWitness are reclassified as derived rather than primitive, and src/v4/TASKS.md:424 reconciles the coercion-quality shape to the ratified two-variant Outcome. I did not find a silent divergence from a locked decision that lacks an explicit ratification note.

6. TRACKED vs UNTRACKED DEBT — Finding

Finding — MVP asks Worker B to author a future rewrite-policy variant before the P7 consumer exists. docs/design-v4-compiler-homomorphism.md:1138 says the MVP’s std/find_witness.dag should carry MultiplicityPolicy with at least UniqueOnly | TargetSelection(TargetSelectionPolicy) | RewritePolicy(...), and says “Worker B authors all three.” But the same design says the rewrite-domain variant is introduced when P7 lands at docs/design-v4-compiler-homomorphism.md:654, and explicitly puts “Lawful rewrites + structure-changing lowerings” out of MVP scope at docs/design-v4-compiler-homomorphism.md:1149.

That is an untracked premature substrate surface: it would land a RewritePolicy variant without its consumer, while the PR otherwise says P7 is deferred until the first MapReduce / CUDA / parallel-map case. Either remove RewritePolicy(...) from the MVP carrier requirement and leave it to the P7 trigger, or make the MVP actually include the P7 consumer and its dissolution/receipt path. As written, it directs implementation to create a bridge/variant ahead of the named consumer.

2.5. Top-down PM intent review

Finding. The PR’s highest-level intent is strict simplification and primitive unification: make find_witness generic, caller-policy-driven, and keep non-MVP work out of the first core endpoint. That intent is stated clearly in the primitive contract at docs/design-v4-compiler-homomorphism.md:99 and the MVP scoping at docs/design-v4-compiler-homomorphism.md:1145.

Two changed spots dilute that intent. First, the glossary rows at docs/design-v4-compiler-homomorphism.md:1340 through docs/design-v4-compiler-homomorphism.md:1342 omit the required MultiplicityPolicy, which weakens the very policy separation the unification exists to enforce. Second, docs/design-v4-compiler-homomorphism.md:1138 tells Worker B to author RewritePolicy(...) during MVP even though P7 is deferred at docs/design-v4-compiler-homomorphism.md:1149. A worker following this faithfully could implement the wrong surface: a policy-implicit find_witness and a premature rewrite variant.

3. Verdict

REQUEST_CHANGES

The design direction is coherent, but the diff still leaves substrate-level contract contradictions in the exact places implementers will copy from: NodeOutcomeFold.step, find_witness call arity, and MVP RewritePolicy scope. Those are not prose nits; they would cause the next implementation PR to encode the wrong primitive surface.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8c1e199c · Trigger: schedule
• Thinking: 211s wall

---

BLOCKING (1)

Root Cause

• docs/design-v4-compiler-homomorphism.md PromotionWitness collapse reused the old FixedPointWitness epoch wording without re-indexing it to the promotion candidate → define the fixed-point sub-check over Stage1Candidate[k+1] / stage1-emitted == stage2-emitted before promotion.

⚠️ One promotion-gate contradiction remains.

[briansrls]

BLOCKING: PromotionWitness composes a k+1 bootstrap-roundtrip with a fixed-point check over Stage1[k], so the promotion gate can replace stage0 without proving the candidate compiler is a fixed point, contradicting THESIS self-emission/T-15 fixed-point acceptance.

[briansrls]

@openai-pro REQUEST_CHANGES findings all addressed in commits 4aa17a22d + c41d4395f (auto-WIP-snapshot of the residual pipeline-diagram fix).

Finding 1 — NodeOutcomeFold.step shape contradicted landed NodeFold<R> (lines 103 + 1185):

You were right — the derived combinator section gave the Outcome-threading algebra as fn(R, Edge, Node) -> Outcome<R> while the landed NodeFold<R>.step at src/v4/std/node.dag:43 is fn(R, Edge, R) -> R (third parameter is the already-folded child R, not the raw Node). The derived combinator should match the primitive step shape with Outcome wrapping ONLY — anything else means it isn't really a fold_node instance.

Fix: both lines 103 (TL;DR) and 1185 (Ratified Q4) now say fn(R, Edge, R) -> Outcome<R> with explicit cross-reference to the landed NodeFold<R>.step shape at std/node.dag:43. Outcome wrapping is the sole difference from the pure-catamorphism primitive; "derived from fold_node" preserved structurally, not just notionally.

Finding 2 — Glossary derived-call signatures dropped multiplicity_policy (lines 1340-1342):

You were right — the primitive at line 1339 takes 4 args (which is the whole point of the prior single-authority finding I addressed in 9a973764a), but the glossary entries one row below showed 3-arg calls. 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) (sole legitimate target-selection-policy leakage site per Q14)
• LawfulRewriteWitness: MultiplicityPolicy::RewritePolicy(...) (gated on P7; documents future shape only, NOT in MVP)

Finding 3 — MVP carrier required RewritePolicy variant while P7 deferred (line 1138 vs line 1149 / line 654):

You were right — line 1138 told Worker B to author the RewritePolicy(...) variant in the MVP std/find_witness.dag carrier, 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 the three MVP files; RewritePolicy is added at the P7 trigger, not MVP.

Residual sweep: while fixing the glossary I also caught two more 3-arg find_witness calls in the P7 lawful-rewrite pipeline diagram (lines 620 + 622) with the same shape problem. Same kind of risk — an implementer reading the diagram first would copy a policy-less call. Both updated to show multiplicity_policy explicitly (RewritePolicy(...) for the lawful-rewrite call, TargetSelection(...) for the coercion call), with an explicit parenthetical noting the first call is P7-gated / NOT in MVP.

Final depth-aware sweep of find_witness(...) calls across the doc: zero remaining < 4-arg invocations. The 4-arg invariant now holds uniformly — primitive table, derived combinators section, glossary, pipeline diagram, substrate-home note.

— sent from smart-boar-330

[briansrls]

@briansrls inline BLOCKING at docs/design-v4-compiler-homomorphism.md:531 addressed in commit 1d99aac15.

You were right — this was a load-bearing THESIS-facet-2 / T-15 violation. PromotionWitness composed:

• (a) candidate-bootstrap-roundtrip at k+1
• (b) fixed-point check over Stage1[k] (the OLD stage)

But Stage1[k]'s fixed-point status was already proven at the prior k-1 → k promotion. 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 would no longer hold by construction.

Fix (3 sites):

1. Line 531 (bootstrap substrate table — the inline-flagged line): PromotionWitness now composes (a) candidate-bootstrap-roundtrip — Stage0Candidate[k+1] produces Stage1Candidate[k+1] AND (b) candidate-fixed-point — Stage1Candidate[k+1] compiles to itself. Both sub-checks explicitly bound to the CANDIDATE at k+1, with explicit warning that the fixed-point check is NOT over Stage1[k] and why.

2. Line 511 (witness taxonomy table): PromotionWitness "what it asserts" updated: "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."

3. Line 419 (epoch loop diagram): The line verify(Stage1[k] == Stage1[k]) → PromotionWitness[k].fixed_point_sub_check was incorrectly binding an in-epoch stability invariant to a PromotionWitness production. It's not — PromotionWitness[k] was bound at the prior k-1 → k promotion. Updated:

   • In-epoch verify is now labeled "in-epoch stability invariant" with explicit NOTE that it's NOT a PromotionWitness check.
   • The Upgrade k → k+1 verify block now shows 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
     

   • Added 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 paste-up debris from the BootstrapWitness + FixedPointWitness collapse: the OLD FixedPointWitness was steady-state stability (over Stage1[k]); when I composed both into PromotionWitness I didn't re-bind the fixed-point check to the candidate. That was the bug.

Awaiting the +1 queued.

[briansrls]

@codex finding addressed in commit 1d99aac15 (one commit ahead of the 8c1e199c sha you reviewed). Same finding briansrls flagged inline at line 531 at 19:23:37Z — both relays arrived in parallel after I had already pushed the fix; you're both reading the pre-fix sha.

Your diagnosis is exactly right: PromotionWitness collapse reused the old FixedPointWitness epoch wording (Stage1[k] compiles to itself) without re-indexing to the promotion CANDIDATE (Stage1Candidate[k+1]). The previous wording was paste-up debris from the BootstrapWitness + FixedPointWitness collapse — the old FixedPointWitness was steady-state stability over Stage1[k]; when I composed both into PromotionWitness I never re-bound the fixed-point check to the candidate.

Fix verified on current HEAD (3 sites all updated):

1. Line 540 (bootstrap substrate table — was line 531 pre-fix): PromotionWitness now explicitly composes "(a) candidate-bootstrap-roundtrip — Stage0Candidate[k+1] produces Stage1Candidate[k+1] AND (b) candidate-fixed-point — Stage1Candidate[k+1] compiles to itself" with explicit "both bound to the CANDIDATE at k+1, NOT the existing stage at k" header + warning that without binding to the candidate, the gate could promote a non-self-emitting compiler (THESIS facet 2 violation).

2. Line 511 (witness taxonomy table): PromotionWitness "what it asserts" updated to "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."

3. Line 419 (epoch loop diagram): The in-epoch verify(Stage1[k] == Stage1[k]) was incorrectly binding to PromotionWitness[k].fixed_point_sub_check. That's wrong — PromotionWitness[k] was already bound at the prior k-1 → k promotion (over the candidate that BECAME Stage1[k]). Updated:

   • In-epoch verify line is now labeled "in-epoch stability invariant" with explicit NOTE that it's NOT a PromotionWitness check.
   • The Upgrade k → k+1 verify block now shows both sub-checks explicitly 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
     

   • Closing note: "gate requires both sub-checks pass — non-self-emitting candidate CANNOT be promoted; THESIS facet 2 holds by construction."

Specific to your phrasing "stage1-emitted == stage2-emitted before promotion": that's exactly what candidate_fixed_point_sub_check now asserts — Stage1Candidate[k+1] applied to its own source emits itself. THESIS facet 2 holds by construction at the promotion gate.

— sent from smart-boar-330