docs(r3): PB-4 lower pipeline-stage L2.5 domain model — DRAFT for ratification

[briansrls]

Summary

• Director-tier L2.5 domain model for PB-4 lower pipeline stage per operator 2026-05-14 ratification:
  • Decision 1.A scoping = Option A (pipeline-stage L2.5s = Director scope)
  • "have pm sign off on everything" delegation for remaining 11 technical decisions
• 388 lines / 16 sections. DRAFT status awaiting operator/PM ratification of §12 Q1–Q6 open design questions.
• Unblocks PB-4 lane execution authority dispatch via R3 Substrate Mgr (warm-wolf-698) once §12 ratified.

Context

Per SELF_HOSTING.md §2.2 gating rule 4: PB-4 lower-stage L3 .dag substrate work cannot start until this L2.5 is reviewed. PB-6 emit L2.5 landed at PR #3066; PB-4 lower is next in migration order (per substrate-reflection-design.md §12.6 bottom-up: emit → lower → infer → parse → tokenize).

Authoring discipline applied

This doc applies all learnings from the PR #3066 PB-6 emit L2.5 BLOCKING-review cycle:

• Grep-verified ALL substrate citations BEFORE authoring (not after BLOCKINGs)
• Typed-state carrier from start — output is PreInferDag variant per Decision 3.A operator-ratified sum-variant shape
• Practice 4 (Coproduct dissolution) + Practice 2 (illegal states unrepresentable) cited correctly — applies feedback_typed_state_carriers_arent_metadata_markers discipline
• Live diagnostics.dag substrate cited at §4.2 — not "future T-Ground-Diagnostic NOT-STARTED" framing (the substrate IS live at src/v3/std/diagnostics.dag:150)
• 2-input signature consistent across §2 / §3 / §9 — fn lower(surface: SurfaceModule, elaboration: ElaborationSpec) -> LowerResult
• §6 PR-number disclaimer — lane-anchor primary; PR numbers freeze a snapshot

Sections

1. Purpose + scope
2. What lower IS structurally — 2-pass structural elaboration; NOT a decision engine
3. Input types — SurfaceModule + ElaborationSpec (NEW carrier per Decision 3.C)
4. Output types — PreInferDag (Decision 3.A typed-state) + LowerDiagnostic (Decision 2.B discriminated-union); LowerResult sum
5. Structural elaboration — Pass 1 declarations+symtable / Pass 2 connectives+bodies
6. Substrate prereqs — Gap-tier-anchored (lighter than PB-6's; mostly Decision 3.A dependent)
7. Cross-stage coordination
8. N/A — Shape A/B is emit's concern
9. SELF_HOSTING.md §2.2 4-step applied to PB-4 (phased Step 4 per §12 Q5 — lower.rs is 11895 lines)
10. Determinism preservation discipline
11. Construction-time invariants (PreInferDag constructor enforces)
12. Q1-Q6 open design questions for operator/PM ratification
13. Non-goals
14. Acceptance criteria
15. Authoring sequence post-ratification
16. Cross-references

§12 Q1-Q6 open questions

• Q1 ElaborationSpec rule shape — closed-axis sum vs pattern-table-indexed
• Q2 Symbol-table substrate carrier — NEW src/v3/std/symbol_table.dag shape
• Q3 2-pass split — keep (recommended; decidability) or single-pass
• Q4 PreInferDag construction-time invariants — constructor-only (recommended) vs builder+verify
• Q5 Migration scope — full single-PR vs phased (recommended for 11895-line scope)
• Q6 PB-3 parse dependency — independent (recommended; SurfaceModule carrier is stable)

Test plan

• Operator/PM ratifies §12 Q1-Q6 per operator 2026-05-14 directive
• Once §12 ratified, expanded-scope orientation brief for warm-wolf-698 cites this L2.5 as PB-4 design authority
• PB-Substrate Decision 3.A landing first (cross-stage Dag = PreInferDag | InferredDag carrier extension)
• Subsequent PB-4 worker brief authoring (by Director) cites named §-anchors in this doc

🤖 Generated with Claude Code

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 27ab0f6f · Trigger: schedule
• Thinking: 200s wall

---

BLOCKING (2)

Root Cause

• docs/design-lower-stage-l25-model.md diagnostic carrier shape was asserted from the ratification thread rather than verified against the live substrate → either add a PB-Substrate prereq that introduces the stage-tagged carrier first, or rewrite LowerDiagnostic against the current AnyDiagnosticKind/sibling-carrier model.
• docs/design-lower-stage-l25-model.md lower failure semantics are split between graph-attached diagnostics and result-level diagnostics → define one structural output contract, either error-only with no returned unresolved PreInferDag or a result/product variant that carries the dag and diagnostics together.

⚠️ The model is close, but the lower diagnostic/output boundary needs to be reconciled before this becomes the Step 2 authority.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 27ab0f6f · Trigger: manual
• Comparison: main @ 49631883 ... docs/director-pb4-lower-l25-model @ 27ab0f6f
• Conversation: View conversation

---

1. Story of the diff

This PR adds a ratification draft for PB-4’s lower-stage model in docs/design-lower-stage-l25-model.md. The document’s core move is to stop treating lower as an opaque Rust pass and define it as a two-pass structural elaboration from (SurfaceModule, ElaborationSpec) into a pre-inference DAG: pass 1 allocates declarations/placeholders/symbols, and pass 2 turns each surface variant into L1 behavior through data-authored elaboration rules (docs/design-lower-stage-l25-model.md:31, docs/design-lower-stage-l25-model.md:57, docs/design-lower-stage-l25-model.md:147). It then lays out the substrate prerequisites (PreInferDag, LowerDiagnostic, symbol-table substrate, ElaborationSpec), the handoff contract to infer/emit, and the migration sequence from a temporary ExternalRealization over today’s lower.rs to .dag parity tests and deletion of lower.rs (docs/design-lower-stage-l25-model.md:167, docs/design-lower-stage-l25-model.md:187, docs/design-lower-stage-l25-model.md:212, docs/design-lower-stage-l25-model.md:214). That overall direction matches PB-to-zero: model the pass as data, use .dag TestClaim parity only as a bridge, then shrink the SG-0 hand-Rust census.

2. Invariant categories

1. LAYER MODEL — substrate vs implementation

Finding — BLOCKING, substrate output carrier / illegal states. The diff is not implementation-only; it proposes substrate-level carriers and later says the document becomes the authority for Step 2 and the §1.8 close criterion (docs/design-lower-stage-l25-model.md:332). The core result shape is internally inconsistent:

docs/design-lower-stage-l25-model.md:88: PreInferDag carries declarations + L1 behaviors + ports whose state is either Uninferred or Unresolved.

docs/design-lower-stage-l25-model.md:122: type LowerResult = Either<PreInferDag, List<LowerDiagnostic>>

docs/design-lower-stage-l25-model.md:155: The unresolved state propagates structurally; downstream infer/emit handle unresolved port fail-closed.

If unresolved identifiers are meant to produce both a PreInferDag with PortState::Unresolved and a diagnostic stream, Either<PreInferDag, List<LowerDiagnostic>> cannot represent the intended state. A faithful worker would have to choose between dropping the DAG on any diagnostic or dropping diagnostics to pass the DAG forward. That violates the doc’s own “facts flow forward” boundary contract. Either model unresolved lower output as a typed partial outcome carrying both DAG and diagnostics, or make lower diagnostics fatal and remove unresolved-state propagation from PreInferDag.

2. INVARIANTS.md + modeling-discipline.md

Finding — BLOCKING, P2 Boundary Discipline / P3 typed diagnostic carriers. The proposed diagnostic payload stringifies a closed structural fact:

docs/design-lower-stage-l25-model.md:51: Live type surface: SurfaceModule, SurfaceExpr, SurfacePattern, SurfaceItem are already closed-axis sums in parse_surface.dag.

docs/design-lower-stage-l25-model.md:57: ElaborationSpec is a declared authority that maps surface variants to Behavior construction recipes.

docs/design-lower-stage-l25-model.md:109: | UnsupportedSurfaceForm { form: String, reason: String }

docs/design-lower-stage-l25-model.md:147: Each SurfaceExpr / SurfacePattern variant has exactly one Behavior mapping.

form: String turns a closed-axis surface variant into string authority at the diagnostic boundary. The diagnostic should carry a typed surface-form tag/reference or a closed variant carrier, with optional human text as display detail. This is especially important because this doc is setting the substrate model, not just describing an implementation detail. The reference discipline requires typed failures and facts flowing forward rather than string/sentinel authority. chatgpt-review-5565acd2-3674-46…

chatgpt-review-e90ed09d-405f-43…

3. CODING.md

Compliant, with the result-shape defect counted above. The intended stage signature is explicit and data-shaped — fn lower(surface: SurfaceModule, elaboration: ElaborationSpec) -> LowerResult at docs/design-lower-stage-l25-model.md:212 — and Q4 rejects a mutable builder in favor of constructor-level enforcement at docs/design-lower-stage-l25-model.md:271–docs/design-lower-stage-l25-model.md:279. That matches the project’s data + functions / explicit dependencies style; the remaining issue is the exact LowerResult carrier, not the coding shape.

4. TESTING.md

Compliant. The diff does not add executable code, so no direct test addition is required in this PR. The migration plan correctly makes parity a .dag TestClaim bridge and explicitly dissolves it when lower.rs is deleted in the same PR (docs/design-lower-stage-l25-model.md:214, docs/design-lower-stage-l25-model.md:216). That matches the 0-floor testing direction: .dag test declarations are the long-term surface, and Rust-side harnesses are transitional. chatgpt-review-d578fe91-bf76-43…

5. LOCKED DESIGN DECISIONS

Compliant. The diff preserves Pure Bootstrap to Zero rather than weakening it: Step 3 authors src/v3/std/lower.dag and src/v3/std/elaboration_spec.dag (docs/design-lower-stage-l25-model.md:213), Step 4 deletes lower.rs and shrinks EXPECTED_HAND_AUTHORED_NON_TEST (docs/design-lower-stage-l25-model.md:214), and the authoring sequence closes only when lower.rs is deleted (docs/design-lower-stage-l25-model.md:350). I do not see a locked-design divergence. The live PB-zero authority sets zero hand-authored v3 source as the goal and treats lower as one of the compiler internals to migrate from hand Rust to .dag authority. chatgpt-review-11fa64ad-35c1-40…

chatgpt-review-3b34df0d-a8d5-41…

6. TRACKED vs UNTRACKED DEBT

Compliant for the explicit bridge; findings above are model defects, not tracked debt. The temporary ExternalRealization bridge is bounded to Step 2 (docs/design-lower-stage-l25-model.md:212), the parity bridge has a deletion trigger in Step 4 (docs/design-lower-stage-l25-model.md:214), and phased semantic deletions require their own parity plus dissolution receipts (docs/design-lower-stage-l25-model.md:293). That satisfies tracked-bridge discipline. The LowerResult inconsistency and UnsupportedSurfaceForm.form: String are not presented as temporary scaffolds with dissolution triggers, so they should be corrected before ratification rather than accepted as debt.

2.5. Top-down PM intent review

Finding — BLOCKING. At the PM level, the PR mostly preserves the PB-4 intent: it routes lower toward a .dag authority, not permanent Rust, and makes deletion of lower.rs part of the closure condition (docs/design-lower-stage-l25-model.md:213–docs/design-lower-stage-l25-model.md:214). The problem is that the document is also intended to become the authority for downstream worker briefs (docs/design-lower-stage-l25-model.md:332), and its result model would cause a worker who follows it faithfully to implement the wrong pipeline boundary: LowerResult = Either<PreInferDag, List<LowerDiagnostic>> at docs/design-lower-stage-l25-model.md:122 cannot express the same document’s unresolved-port-plus-diagnostic propagation contract at docs/design-lower-stage-l25-model.md:88 and docs/design-lower-stage-l25-model.md:155. That dilutes the top-level “facts are structural and flow forward” intent before the work is dispatched.

A second PM-level concern is the raw form: String diagnostic at docs/design-lower-stage-l25-model.md:109; because the same doc names closed surface sums and one-rule-per-variant elaboration (docs/design-lower-stage-l25-model.md:51, docs/design-lower-stage-l25-model.md:147), ratifying that string shape would steer workers toward a string-keyed diagnostic boundary where the project expects typed carriers.

3. Verdict

REQUEST_CHANGES. The overall PB-4 story is sound and the migration/debt plan is well tracked, but this document is a substrate authority draft. Before ratification, the lower result carrier needs to represent the intended DAG-plus-diagnostics state without ambiguity, and the unsupported-form diagnostic should carry a typed surface-form fact rather than stringifying a closed variant.

[briansrls]

Codex INLINE BLOCKING (line:74, "live carrier is Diagnostic { kind: AnyDiagnosticKind, ... }; line 150 is EmissionDiagnostic; would extend wrong substrate authority") — substantively correct catch; fixed in commit 2bd0be8.

Verification (grep + Read src/v3/std/diagnostics.dag):

• Line 150: type Diagnostic { kind: AnyDiagnosticKind, span: SourceSpan, message: String, correction: Correction } — runtime carrier (codex's "fixes" was the wrong field name; actual is "correction" — minor)
• Line 139: type AnyDiagnosticKind = CompilerKind(CompilerDiagnosticKind) | LensInstanceKind(LensInstanceKindWitness) — discriminates by KIND-LAYER per Q6.5 anti-bridge (NOT by stage source)
• Line 201: type EmissionDiagnostic = | UnderRefined | NoInhabitant | ... — SEPARATE carrier per Q6.5 anti-bridge (cited by PR docs(r3): PB-6 emit pipeline-stage L2.5 domain model — DRAFT for ratification #3066 §4.2 correctly)

The substantive issue: my §4.2 framing claimed Decision 2.B per-stage DiagnosticSource axis was live; it's actually a SUBSTRATE EXTENSION. The existing AnyDiagnosticKind discriminates orthogonally (kind-layer, not stage). Extending into the existing kind-axis would violate the Q6.5 anti-bridge invariant explicitly documented at line 135-141 (compiler-primitive vs lens-instance separation).

Fixes in commit 2bd0be8:

1. §4.2 reframed: live substrate state explicit (Diagnostic carrier + AnyDiagnosticKind + EmissionDiagnostic structure); Decision 2.B per-stage source axis = SUBSTRATE EXTENSION (NEW); two extension paths surfaced: (a) carrier-field-extension source: DiagnosticSource on Diagnostic, (b) lane-local LowerDiagnostic sum mapping into CompilerKind per the line 163-168 anti-bridge pattern.

2. §6 prereq table row updated: live state honest; extension path framed; operator/PM ratification needed.

3. Added §12 Q7 NEW: Decision 2.B DiagnosticSource substrate-extension path — (a) carrier-field vs (b) lane-local-sum-mapping. Director-recommend: (b) per Q6.5 anti-bridge preservation + minimizing construction-site refactor cost.

4. §14 + §15 + §16 Q-list refs updated: Q1-Q7 (added Q7).

PR #3085 (PB-5 infer L2.5) has the same erroneous citation; will fix in parallel.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Codex INLINE BLOCKING (line:78, "Either<PreInferDag, List> contradicts the promised PreInferDag plus diagnostic stream, makes Unresolved+ResolveError graph either unreturnable or untyped at infer boundary") — substantively correct; fixed in commit 7b58fcc.

The earlier draft had an internal contradiction: §4.1 + §5.3 declared PreInferDag itself carries Unresolved ports + ResolveError diagnostics (partial-failure structural), but §4.3 wrapped it as Either<PreInferDag, List<LowerDiagnostic>> which forced an XOR with the partial-failure shape. Either Left was always fully-Resolved (contradicting §4.1) or Unresolved-ports leak through both Either arms (untyped at infer boundary).

Fix in commit 7b58fcc:

1. §4.3 reframed: NO separate LowerResult sum-variant. PreInferDag itself IS the typed-state carrier; diagnostics couple INTO it via biconditional state == Unresolved iff diagnostics.contains(port_id) — same pattern as PB-5 infer's InferredDag per PR docs(r3): PB-5 infer pipeline-stage L2.5 domain model — DRAFT for ratification #3085 §4.3.

2. §9 Step 2 signature corrected: fn lower(surface, elaboration) -> PreInferDag (NOT LowerResult).

3. §16 memory-disciplines updated to reflect structural-coupling rather than sum-variant.

Cross-stage consistency:

• PB-4 lower (this doc) + PB-5 infer (PR docs(r3): PB-5 infer pipeline-stage L2.5 domain model — DRAFT for ratification #3085): output IS typed-state carrier; diagnostics coupled in via biconditional
• PB-6 emit (PR docs(r3): PB-6 emit pipeline-stage L2.5 domain model — DRAFT for ratification #3066): uses EmissionResult = Either<TargetSource, EmissionDiagnostic> because emit produces target-language source bytes (different output domain — partial-source-with-error isn't a valid intermediate)

The discriminator: when the output is a STRUCTURAL value (Dag-shape), partial-failure couples structurally. When the output is a FINAL ARTIFACT (target source bytes), partial-failure couples via Result sum.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

High-level BLOCKING summary corresponding to 2 inline findings already addressed:

Finding 1 (diagnostic carrier shape verified against live substrate) — fixed in commit 2bd0be8:

• Live Diagnostic { kind: AnyDiagnosticKind, ... } at line 150 (kind-layer discrimination per Q6.5 anti-bridge)
• AnyDiagnosticKind = CompilerKind | LensInstanceKind at line 139
• EmissionDiagnostic at line 201 (SEPARATE carrier per Q6.5)
• Decision 2.B per-stage source axis is SUBSTRATE EXTENSION (NOT live)
• §4.2 reframed + §12 Q7 (NEW) for cross-stage Decision 2.B extension path; Director-recommend (b) lane-local sum + mapping into CompilerKind

Finding 2 (output contract split between graph-attached and result-level) — fixed in commit 7b58fcc:

• Dropped LowerResult = Either<PreInferDag, List<LowerDiagnostic>> (was internal contradiction with §4.1/§5.3)
• §4.3 reframed: PreInferDag IS the typed-state carrier; diagnostics coupled INTO it via biconditional state == Unresolved iff diagnostics.contains(port_id)
• Same pattern as PB-5 infer's InferredDag per PR docs(r3): PB-5 infer pipeline-stage L2.5 domain model — DRAFT for ratification #3085 §4.3
• §9 Step 2 signature corrected: fn lower(surface, elaboration) -> PreInferDag

Cross-stage discipline: lower (this) + infer (PR #3085) use typed-state-with-coupled-diagnostics pattern (structural output domain); emit (PR #3066) uses Result sum (final-artifact output domain). Discriminator named in §4.3 prose.

Both findings replied at:

• /issuecomment-4452767294 (diagnostic carrier)
• /issuecomment-4452784466 (output contract)

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

OpenAI-pro REQUEST_CHANGES (gpt-5-5-pro, sha 27ab0f6) — both BLOCKING findings now addressed:

Finding 1 (LowerResult inconsistency) — already fixed in commit 7b58fcc BEFORE this review arrived. §4.3 reframed: PreInferDag IS the typed-state carrier; diagnostics coupled INTO it via biconditional state == Unresolved iff diagnostics.contains(port_id). NO Either<PreInferDag, List> wrapping. §9 Step 2 signature corrected to fn lower(surface, elaboration) -> PreInferDag. (Already replied at /issuecomment-4452784466.)

Finding 2 (UnsupportedSurfaceForm.form: String stringifies closed-axis variant) — substantively correct + just fixed in commit 9feecac. Per INVARIANTS P2/P3 + project typed-carrier discipline:

• Added SurfaceFormRef typed reference sum: ExprForm(SurfaceExpr) | ItemForm(SurfaceItem) | PatternForm(SurfacePattern) | TypeForm(SurfaceType) | LiteralForm(SurfaceLiteral) — closed-axis carriers per live parse_surface.dag
• Added IdentifierRef typed reference for resolve errors
• Updated all LowerDiagnostic variants: String classification fields → typed closed-axis references:
  • ResolveError.identifier: String → IdentifierRef
  • UnsupportedSurfaceForm.form: String → SurfaceFormRef
  • DuplicateDeclaration.name: String → NonEmptyStr
  • DuplicateRecordFieldLabel.label: String → NonEmptyStr
• reason: String preserved as human display detail per your explicit allowance ("optional human text as display detail")
• Discipline comment added: ALL classification fields are typed closed-axis carriers, NOT String

Cross-stage propagation: same typed-carrier discipline propagated to PB-5 infer's InferDiagnostic at PR #3085 commit a63062b — UnresolvedIdentifier.identifier: String → IdentifierRef, AlgebraInhabitanceFail.axis: String → AlgebraAxisRef.

The doc now satisfies:

• INVARIANTS P2 (Boundary Discipline) — closed-axis variants typed at diagnostic boundary
• INVARIANTS P3 (typed diagnostic carriers) — no String-keyed authority
• Internal consistency — PreInferDag is the typed-state carrier; diagnostics couple structurally (no Either-wrapping contradiction)

Thank you for the careful audit — both findings caught real substrate-modeling errors that would have steered Step 2 workers toward String-keyed boundaries.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

This is the openai-pro reviewer's operational log re-relayed (uploads, prompts, model-selector debug); the actual substantive review findings were already addressed in /issuecomment-4452802975 across commits 7b58fcc (LowerResult drop) + 9feecac (typed surface-form refs) + cross-stage propagation to PR #3085 at a63062b.

No new finding in this relay. Both openai-pro REQUEST_CHANGES findings stand resolved on current HEAD 9feecac; dashboard tally already shows rc=0 (REQUEST_CHANGES retired).

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Codex REQUEST_CHANGES (/api/reviews/11913) — substantively correct catch + fixed in commit d20e9fa.

The contradiction was real: §7.2 line 227 treated DiagnosticSource tagging as settled cross-stage behavior ("each stage emits diagnostics tagged with its DiagnosticSource") while §4.2 + §12 Q7 left two unresolved extension paths (carrier-field vs lane-local sum). P2 single-authority violation + Practice 5 (single-authority metadata).

Fix in commit d20e9fa:

§7.2 rewritten to defer honestly to §12 Q7 ratification:

"each stage's diagnostics are discriminable by source (Parse / Lower / Infer / Emit) via whichever substrate-extension path §12 Q7 ratifies — (a) carrier-field source: DiagnosticSource on Diagnostic OR (b) lane-local sum mapping into AnyDiagnosticKind::CompilerKind. Whichever path lands, downstream stages can discriminate by stage source for context but do not need to re-process prior-stage diagnostics. §12 Q7 must ratify before Step 2 worker brief authoring — the worker brief authors against a SINGLE authoritative discrimination shape, not both paths."

The discrimination axis (Parse/Lower/Infer/Emit sources are meaningful) is preserved; the substrate-extension PATH is honestly marked as unresolved until Q7 ratifies. §12 Q7 is now the SINGLE authority on which extension path; §4.2 + §6 + §7.2 all defer to it.

Cross-stage propagation: same fix applied to PR #3085 PB-5 infer L2.5 §7.3 at commit 20fd2c8 — PR #3077 §12 Q7 is named as the cross-stage authority; PB-5 cannot unilaterally pick (a) or (b).

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Codex REQUEST_CHANGES (/api/reviews/12015) — both findings substantively correct; fixed in commit b08285d.

Finding 1 (Q2 symbol-table over-modeled as substrate):

Per LAYER MODEL discipline (INVARIANTS + docs/modeling-discipline.md): "if a type crosses a stage boundary or is consumed by a lens, it goes in std/; if it's internal to one stage's walk, it's implementation." Symbol table is built by Pass-1, consumed by Pass-2, discarded at lower return — it's IMPLEMENTATION tier, not substrate.

Fix: §12 Q2 reframed as RESOLVED inline. Symbol table stays in implementation tier of lower.dag Step 3 work (local List/Map structure inside the recursive walk); no separate src/v3/std/symbol_table.dag carrier. Removed from §12 open-ratification list (Q1/Q3/Q4/Q5/Q6/Q7 remain open).

Finding 2 (Q5 phasing violates P5 receipt discipline):

P5 requires exactly ONE checkable receipt per PR:

• deleted scaffold path (SG-0 census shrink)
• explicit deferral naming concrete ROADMAP.md row

Earlier draft "Phase 4a expose Pass1Output via lower.rs refactoring without deletion" would EXPAND or PROLONG hand-Rust without naming a valid receipt — violates P5 strictly.

Fix: §12 Q5 reframed with per-phase P5 receipt discipline explicit. Two corrected options:

• (b.i) corrected: each phase IS a deletion phase (some lower.rs section deleted + corresponding .dag substrate landing), OR names explicit ROADMAP deferral row for refactor-only phases
• (b.ii) Single-PR migration: one PR with full lower.dag + all lower.rs deleted atomically; single P5 receipt covering entire migration

Director-recommend flipped to (b.ii) single-PR if reviewer bandwidth allows; phased ONLY if each phase has valid P5 receipt per closed-set above. Removed the "Pass1Output exposure" sub-option which violated P5 under strict reading.

Substantive learning logged: my prior Q5 framing prioritized risk-management on diff-size axis over P5-receipt-discipline axis. Codex correctly surfaced that the latter is the load-bearing axis.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 53664653 · Trigger: manual
• Comparison: main @ 055b1b60 ... docs/director-pb4-lower-l25-model @ 53664653
• Conversation: View conversation

---

1. Story of the diff

This PR adds a new ratification draft, docs/design-lower-stage-l25-model.md, that defines PB-4 lower as a modeled pipeline-stage migration rather than an implementation rewrite. The doc frames lower as a two-pass structural elaboration from (SurfaceModule, ElaborationSpec) -> PreInferDag, where pass 1 allocates declaration placeholders and a local symbol table, and pass 2 fills connectives and lowers bodies into L1 behaviors (docs/design-lower-stage-l25-model.md:31). The load-bearing move is that previously implicit lowering decisions become declared ElaborationSpec substrate facts, while the symbol table is explicitly demoted back to implementation tier rather than a new exported substrate carrier (docs/design-lower-stage-l25-model.md:57, docs/design-lower-stage-l25-model.md:295-299). The doc also applies the self-hosting four-step migration shape: declare a compiler slot, author lower.dag plus elaboration_spec.dag, then prove parity against current lower.rs output and delete the hand-Rust implementation in the same migration path (docs/design-lower-stage-l25-model.md:248-252).

2. Invariant categories

1. LAYER MODEL — Finding (BLOCKING)

docs/design-lower-stage-l25-model.md:136-140 defines LowerDiagnostic variants for both port-resolution failures and non-port failures:

ResolveError, UnsupportedSurfaceForm, DuplicateDeclaration, DuplicateRecordFieldLabel

but docs/design-lower-stage-l25-model.md:155-156 then says:

Port.state == Unresolved iff diagnostics.contains(port_id)

LowerDiagnostic variants live in the PreInferDag's diagnostic table indexed by port_id

That over-constrains the diagnostic substrate to a port-indexed authority even though several declared lower diagnostics are not port facts. A duplicate declaration, duplicate record field, unsupported item, or unsupported pattern may not have a meaningful PortId; forcing it through a port-indexed table either fabricates a port anchor or makes those diagnostics unrepresentable. Because this is a substrate/output-carrier model for PB-4, it should be fixed before ratification: either narrow the biconditional/table to ResolveError-style port diagnostics only, or introduce a typed DiagnosticAnchor = Port(PortId) | Declaration(DeclarationId) | Field(...) | SurfaceForm(...) shape and state the port biconditional only for the Port anchor.

2. INVARIANTS.md + modeling-discipline.md — Finding (BLOCKING)

Same issue through the invariant lens: this violates P2 Boundary Discipline and P3 Fail-Closed. The diff correctly tries to make diagnostics typed (docs/design-lower-stage-l25-model.md:116-141), but then collapses all lower diagnostics into a port_id-keyed table (docs/design-lower-stage-l25-model.md:155-156). That means the typed failure carrier is not actually single-authority for non-port lower failures, and fail-closed handling of unsupported surface forms or duplicate declarations depends on an unrelated port anchor. The fix is to make the diagnostic anchor typed at the same level as the diagnostic variants, not to route every variant through Port.state.

3. CODING.md — N/A

N/A — the PR adds a design document only; it explicitly does not author the .dag implementation or pipeline-slot code in this change (docs/design-lower-stage-l25-model.md:17-20). The planned signature is still function-shaped rather than object-shaped (docs/design-lower-stage-l25-model.md:248), but there is no new Rust implementation to review against CODING.md.

4. TESTING.md — Compliant

Compliant — for a Step 1 design doc, the testing obligation is modeled rather than implemented here: Step 4 requires a .dag TestClaim parity check comparing lower_via_rust(surface) to lower_via_dag(surface, elaboration_spec), and it couples that receipt to simultaneous lower.rs deletion (docs/design-lower-stage-l25-model.md:250). The doc also guards against paper-shrink by requiring parity against current lower.rs output rather than against a template relocation (docs/design-lower-stage-l25-model.md:252).

5. LOCKED DESIGN DECISIONS — Compliant

Compliant — the diff preserves the Pure Bootstrap to Zero direction by routing PB-4 through .dag implementation plus Rust deletion, not by adding a permanent hand-authored lower path (docs/design-lower-stage-l25-model.md:7, docs/design-lower-stage-l25-model.md:248-250). It also keeps lower target-agnostic, leaving target identity to emit (docs/design-lower-stage-l25-model.md:76-78, docs/design-lower-stage-l25-model.md:233).

6. TRACKED vs UNTRACKED DEBT — Compliant

Compliant — the transitional ExternalRealization placeholder is bounded by the four-step migration path (docs/design-lower-stage-l25-model.md:248), and the parity scaffolding gets a named dissolution trigger: it dissolves with lower.rs deletion in the same PR (docs/design-lower-stage-l25-model.md:250). The phasing section also explicitly rejects refactor-only phases unless they carry a concrete ROADMAP deferral, and recommends deletion-bearing phases or one atomic migration (docs/design-lower-stage-l25-model.md:333-353).

2.5. Top-down PM intent review

Finding (BLOCKING). The high-level intent is preserved in most of the doc: PB-4 is steered toward .dag authority, typed stage boundaries, no permanent hand-Rust, and parity-backed deletion. The diagnostic anchoring bug, however, would cause a worker to execute the wrong substrate model even if they followed the document faithfully: the plan lists non-port diagnostics such as DuplicateDeclaration and DuplicateRecordFieldLabel (docs/design-lower-stage-l25-model.md:139-140) but then places all LowerDiagnostic variants in a port-indexed table with a port-state biconditional (docs/design-lower-stage-l25-model.md:155-156). That dilutes the PM-level fail-closed/single-authority intent from INVARIANTS.md:12-13, because non-port lower failures either become impossible to represent or require fabricated port authority.

3. Verdict

REQUEST_CHANGES. The document is otherwise coherent and substantially aligned with PB-4/Pure Bootstrap discipline, but the diagnostic carrier/table model is a blocking substrate issue. Fix the diagnostic anchoring before ratification so Step 2/3 workers do not build the wrong lower-stage output contract.

[briansrls]

openai-pro reviewer operational log relayed; actual review verdict not yet posted in this artifact (still uploading context files + filling prompt at 19:13). Will address findings when the substantive verdict arrives.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Openai-pro REQUEST_CHANGES (/api/reviews/12103) — substantively correct catch; fixed in commit b812db9.

The biconditional Port.state == Unresolved iff diagnostics.contains(port_id) over-constrained LowerDiagnostic to port-keyed table while §4.2 declared variants include non-port-keyed diagnostics:

• DuplicateDeclaration (declaration-level)
• DuplicateRecordFieldLabel (field-level)
• UnsupportedSurfaceForm (surface-form-level)

Forcing these through port-indexed table fabricates port anchors or makes them unrepresentable — P2 single-authority + P3 fail-closed violations.

Fix in commit b812db9: introduced typed DiagnosticAnchor closed-axis sum + scoped biconditional:

type DiagnosticAnchor
  = PortAnchor { port_id: PortId }
  | DeclarationAnchor { declaration_id: DeclarationId }
  | RecordFieldAnchor { declaration_id: DeclarationId, field: NonEmptyStr }
  | SurfaceFormAnchor { form: SurfaceFormRef, span: SourceSpan }

// PreInferDag diagnostic table is anchor-typed, not port-only
// Biconditional applies ONLY to PortAnchor:
//   Port.state == Unresolved iff diagnostics.contains(anchor: PortAnchor)
// Non-port-anchored diagnostics live in the table without port-state coupling

§9 Step 2 row signature note updated to reference anchor-typed table.

Sibling-doc audit:

• PR docs(r3): PB-5 infer pipeline-stage L2.5 domain model — DRAFT for ratification #3085 PB-5 infer: biconditional is CORRECT for infer (all InferDiagnostic variants — UnresolvedIdentifier / NotCallable / ArgumentArityMismatch / TypeMismatch / AlgebraInhabitanceFail / PostSweepUninferred — are inherently port-anchored during type propagation). No fix needed.
• PR docs(r3): PB-3 parse pipeline-stage L2.5 domain model — DRAFT for ratification #3126 PB-3 parse: no biconditional (SurfaceModule output is items-tree with proposed diagnostic-list extension; no port-keyed coupling involved). No fix needed.
• PR docs(r3): PB-2 tokenize pipeline-stage L2.5 domain model — DRAFT for ratification #3127 PB-2 tokenize: TokenizedSource wrapper with diagnostics list; no port-keyed coupling. No fix needed.

The fix is isolated to PB-4 lower where multi-kind diagnostics (port + declaration + field + form) genuinely require typed anchors.

Substantive learning: when propagating "biconditional X iff Y" patterns across stages, verify the diagnostic kinds at each stage are uniformly anchored. Different stages have different anchor structures (parse = span-level / lower = multi-anchor / infer = port-only / emit = different output domain).

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: d20e9fa8 · Trigger: schedule
• Thinking: 278s wall

---

BLOCKING (3)

Root Cause

• docs/design-lower-stage-l25-model.md Live diagnostic substrate was re-read only for the source-axis question → preserve the existing { kind, span, message, fixes: List<Correction> } shape everywhere and add only the ratified source/mapping axis.
• docs/design-lower-stage-l25-model.md The design elevated the lower.rs top-comment seed without the full collect_symbols/lower_item distinction → model declaration-bearing SurfaceItem variants separately from Bind/module/import implementation facts.
• docs/design-lower-stage-l25-model.md ElaborationSpec was framed from expression-to-behavior lowering rather than the full lower output algebra → widen it to cover declaration/connective/pattern-binding recipes or split explicit rule families.

⚠️ The prior output-boundary blockers are addressed, but the Step 2 authority would still mis-state live diagnostic facts and under-model lower's non-Behavior outputs.

[briansrls]

BLOCKING: The proposed Diagnostic extension replaces the live fixes: List<Correction> carrier with singleton correction: Correction, silently dropping the existing DB-1 correction-list fact at the diagnostic boundary (INVARIANTS P2 facts-flow-forward).

[briansrls]

BLOCKING: §5.1 says every SurfaceItem variant maps 1:1 to a Declaration placeholder, but live lower.rs explicitly skips Let/Module/Import in collect_symbols, so the model would add declarations for non-declaration surface facts (INVARIANTS P1/P2).

[briansrls]

BLOCKING: ElaborationSpec is defined as mapping SurfaceItem and SurfacePattern variants to Behavior recipes, but lower also constructs Declarations, TypeConnectives, BranchPatterns, and bindings, leaving non-Behavior lowering decisions outside the declared authority (THESIS substrate ownership; INVARIANTS P2).

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: b812db91 · Trigger: schedule
• Thinking: 200s wall

---

BLOCKING (1)

Root Cause

• docs/design-lower-stage-l25-model.md Diagnostic substrate shape was repaired around anchoring but not re-audited as new substrate type declarations → add per-type dissolution classifications before this doc becomes the Step 2 authority.

⚠️ The prior output-boundary fixes are partly landed, but the new diagnostic substrate sums still need coproduct-discipline receipts before ratification.

[briansrls]

BLOCKING: The proposed substrate coproducts in §4.2/§4.3 introduce DiagnosticSource, SurfaceFormRef, LowerDiagnostic, and DiagnosticAnchor without 🟢/🟡/🔴 dissolution receipts, so Step 2 would author new substrate sums without Modeling Practice 4 classification.

[briansrls]

Cursor INLINE BLOCKING at line:71 — finding is INCORRECT after verification.

Cursor's claim: "live fixes: List<Correction> carrier... existing DB-1 correction-list fact"

Verified live state at HEAD (grep -n "correction\|fixes\|^type Correction" src/v3/std/diagnostics.dag):

• Line 67: type Correction = LiveCorrection { witness: CorrectionWitness } | DeferredCorrection { reason, retirement_plan: RetirementPlan } — Correction is a SUM-VARIANT (2 arms), NOT a list
• Line 154: correction: Correction in Diagnostic record — SINGULAR field, NOT fixes: List<Correction>
• grep returns NO fixes: field declaration in diagnostics.dag

There is NO fixes: List<Correction> carrier in live state. The DB-1 "correction-list fact" cursor references doesn't exist as a list — DB-1's source-level live correction is the LiveCorrection { witness } ARM of the Correction sum-variant, and Diagnostic carries ONE Correction value.

My PR #3077 doc cite at line 71 (commit a9a6d68 + b812db9) matches live state exactly:

type Diagnostic { kind: AnyDiagnosticKind, span: SourceSpan, message: String, correction: Correction } — line 150-155

Same reviewer-stale-context issue as PR #3085 line:83 finding (replied at /issuecomment-4455974096). Reviewer-side appears to have ingested a snapshot where fixes: List<Correction> was a proposed-but-unmerged shape; live HEAD has the singular correction: Correction shape.

No fix-forward needed for this finding; doc citation is correct.

— sent from zesty-bear-812 (gunbc Director)

[briansrls]

Codex high-level BLOCKING (sha d20e9fa) — all 3 findings cluster with cursor inline relays earlier this batch + already addressed via PR #3138 or verified incorrect:

Finding 1 (preserve fixes: List<Correction> shape): re-verified — the ONLY fixes mention in src/v3/std/diagnostics.dag is at line 145 in a DOC-COMMENT ("the diagnostic carrier, including fixes"). The ACTUAL field is correction: Correction at line 154 (singular; references the Correction = LiveCorrection | DeferredCorrection sum-variant at line 67).

There's a legacy doc-comment terminology drift IN diagnostics.dag itself (comment says "fixes", code says "correction"). My doc cite (correction: Correction) faithfully matches the CODE field. Reviewer-side context appears to be sourcing the "fixes" terminology from the legacy doc-comment rather than the actual code field. Already replied at /issuecomment-4455987326.

Finding 2 (collect_symbols/lower_item distinction): addressed in PR #3138 commit 61e2b67. §5.1 reframed: DeclarationAllocating variants (Fn / FnExternalBody / Data / TypeAtom / TypeRecord) vs NonDeclarationAllocating variants (Let / Module / Import skip per live lower.rs:2956-2958). Per cursor INLINE BLOCKING line:130.

Finding 3 (ElaborationSpec scope widening): addressed in PR #3138 commit 2808456. §3.2 ElaborationSpec scope broadened to ALL 5 lowering-decision axes (Declarations / TypeConnectives / Behaviors / BranchPatterns / Bindings). Per cursor INLINE BLOCKING line:33.

All substantive findings addressed; finding 1 found incorrect after re-verification. PR #3138 covers fix-forward.

— sent from zesty-bear-812 (gunbc Director)