docs: DB-9 R2.1 — Track 9 substrate integrity primitives graduation

[briansrls]

Summary

Follow-up to PR #511 (merged at R2 post-review f22d5ecf1). #511's
four review blockers (chatgpt-auto-review REQUEST_CHANGES, codex-review
BLOCKING, three inline BLOCKING comments) all converged on one class:
R2's substrate records admitted illegal states and relied on "enforced
by construction" rather than type-shape enforcement. This PR graduates
four substrate integrity primitives into src/v3/std/substrate.dag
and rewrites the DB-9 R2 design records on top of them.

Before (from merged #511):

type Cluster {
  members: List<MemberDescent>                    // admits [] and singletons
  intra_cluster_calls: List<IntraClusterCall>     // admits []
}
type MemberDescent {
  member: NodeId
  position: Int                                   // admits negative / out-of-arity
}
type IntraClusterCall {
  transform: NodeId                               // admits non-Transform
}

After (this PR):

type Cluster {
  members: NonSingletonList<MemberDescent>              // ≥2 by type shape
  intra_cluster_calls: NonEmptyList<IntraClusterCall>   // ≥1 by type shape
}
type MemberDescent {
  member: NodeId
  position: ArityIndex                                  // typed newtype over NonNegativeInt
}
type IntraClusterCall {
  transform: TransformRef                               // typed newtype witnessing Behavior::Transform
}

What lands

1. Four substrate integrity primitives in src/v3/std/substrate.dag:

   • NonEmptyList<T> — cardinality ≥ 1 by type shape
   • NonSingletonList<T> — cardinality ≥ 2 by type shape
   • ArityIndex — typed newtype over NonNegativeInt; paired with arity-bearing carrier
   • TransformRef — typed newtype over NodeId that statically witnesses Behavior::Transform

2. DB-9 R2.1 doc rewrite (docs/design-mutual-recursion-lowering.md):

   • Substrate record declarations use the new primitives
   • Dissolution-receipt paragraph rewritten — no more "enforced by construction" language
   • Revision history + Changelog entries for R2.1
   • Rejected-alternatives row explaining why construction-only invariants were rejected
   • Associations section updated

3. ROADMAP Track 9 entry (ROADMAP.md) — substrate integrity primitives graduation, primitive ledger, planned second consumer (IndexedElement<T>.index in src/v3/std/list.dag), and explicit deferral of the deeper Dag.nodes segregation refactor.

Why a follow-up PR

#511 merged at R2 while the R2.1 design discussion was in progress. The
graduation work is independently valuable (gates any future consumer,
including IndexedElement cleanup) so it lands as a clean follow-up
rather than an amendment to the merged history.

Test plan

• cargo test -p v3-compiler --test m2_substrate_inhabitance_test (3/3 pass — reflection surface, coproduct/runtime carrier parity, Rust/reflected parity)
• cargo test -p v3-compiler --test real_stdlib_parse_smoke (9/9 pass)
• cargo test -p v3-compiler --test l1_5_fixed_point_test pipeline_dag_parses (1/1 pass)
• cargo fmt --all --check (pre-push hook)
• CI green end-to-end
• Review: confirm the four original blockers (from docs: DB-9 R2 — mutual recursion lowers to substrate Loop #511 comments 3101980249, 3101980252, 3102304401, and the chatgpt-auto-review/codex-review on f22d5ecf1) are now answered at the type shape rather than at the producer

🤖 Generated with Claude Code

[briansrls]

ChatGPT Review

Principle audit.

1. FAIL-CLOSED. This looks okay in the landed diff. I do not see a new silent-success path or a “keep going with placeholder state” move; the round is mostly deleting “enforced by construction” prose and trying to surface invariants structurally. The only thing I would watch later is the sketched as_transform(dag, id) -> TransformRef? constructor: when that lands, a bad cast should have a crisp failure story, not a silent None that callers can blur into “not applicable.”

2. ILLEGAL STATES UNREPRESENTABLE. Partially satisfied, with one BLOCKING concern. NonEmptyList<T> and NonSingletonList<T> are real wins: empty and singleton cases move onto the shape itself. But MemberDescent.position is overclaimed. The doc now says negative and out-of-arity positions are “unrepresentable by the type shape” (docs/design-mutual-recursion-lowering.md, diff lines 60, 85-88, 111-116), while the new ArityIndex block explicitly says bound-relative validity is still checked “at the construction site that pairs an ArityIndex with its carrier” (src/v3/std/substrate.dag, diff lines 188-197). That means the type makes non-negativity structural, but the member-relative bound is still behavioral/API-level, not in the data model.

3. FACTS FLOW FORWARD. Satisfied. This round is materially better than R2 on fact preservation: IntraClusterCall stays anchored on the authoritative Transform rather than compressing to caller/callee, and the Track 9 ledger makes the new carriers explicit instead of leaving them as unwritten convention. I do not see a new silent fact-drop in the changed material.

4. COPRODUCT DISSOLUTION. Satisfied. No new substrate enum is introduced here, so there is no new N≥2 Rust enum that needed a fresh terminal/scaffold/dissolve-now receipt. The existing LoopBound receipt remains in-doc, which is the right shape for a substrate stop-signal.

5. SINGLE AUTHORITY. Satisfied. The shift from raw call-edge facts to TransformRef is the right direction: the authoritative callsite stays the Transform node, not a parallel edge payload. I do not see a second source of truth being introduced by NonEmptyList/NonSingletonList; the only issue is that ArityIndex still leaves one important relation outside the shape, not that it duplicates the fact.

6. API-LEVEL ENFORCEMENT. Same BLOCKING issue as #2. NonEmptyList and NonSingletonList are genuinely API-level. ArityIndex is not fully there yet: the new type stops negative integers, but the crucial invariant for this consumer is “this index is valid for this member,” and the diff still places that in constructor prose rather than in the type. So the current check is mixed: structural for cardinality and sign, behavioral for member-relative arity.

Design question. Does MemberDescent really want an ArityIndex, or does it want a first-class reference to an actual formal parameter of member? That is the crux, because if the real invariant is “this points to one of this member’s parameters,” then a bare index still makes downstream code trust a relation that is not carried by the shape and will be tempting to re-check or re-derive later.

Verdict. REQUEST_CHANGES. This is directionally strong, and I think the NonEmptyList/NonSingletonList part is a clean improvement. But I would not bank the “four blockers closed” / “out-of-arity is now unrepresentable by the type shape” claim until either the carrier is strengthened or the docs are softened to say only non-negativity moved into the type.

LOOP HEALTH: converging — this round clearly dissolves real construction-only debt and turns a repeated review theme into an explicit Track 9 pattern, but the ArityIndex half still stops short of the fully structural guarantee the doc now claims.

---

View conversation

[briansrls]

codex · gpt-5.4 · 1ef38dbd

⚠️ Review (blocking: 1, non-blocking: 1+/0-)

BLOCKING (1)

Root Cause

• src/v3/std/substrate.dag primitive declarations landed without the matching consumer-side substrate migration -> either land the actual Cluster/MemberDescent/IntraClusterCall hookup in this PR or rewrite the new comments/docs/roadmap as planned future consumers

Non-blocking — Strengths

• docs/design-mutual-recursion-lowering.md The R2.1 rewrite cleanly retires the old raw-carrier shape at the design level and keeps the five-Behavior constraint intact.

ROADMAP — Verified

• Lane 3 Stage 3a.1 direction: The docs stay aligned on lowering mutual recursion through Loop instead of drifting back to the rejected lens-level SCC design.

ROADMAP — Incomplete

• Track 9 substrate integrity primitives graduation: The ledger is ahead of the substrate authority: the primitives are present, but their advertised first consumers are not yet reflected in src/v3/std/substrate.dag.

⚠️ The modeling direction is right, but this PR currently records Track 9 as graduated before the substrate authority actually uses the new carriers.

[briansrls]

BLOCKING: The new header says these primitives already serve Cluster/MemberDescent/IntraClusterCall, but the checked-in substrate still defines none of those consumers, so the authority file overstates Track 9 graduation and violates thesis-verification/single-authority discipline.

[briansrls]

codex · gpt-5.4 · 1ef38dbd

⚠️ Review (blocking: 1, non-blocking: 1+/0-)

BLOCKING (1)

Root Cause

• src/v3/std/substrate.dag primitive declarations landed without the matching consumer-side substrate migration -> either land the actual Cluster/MemberDescent/IntraClusterCall hookup in this PR or rewrite the new comments/docs/roadmap as planned future consumers

Non-blocking — Strengths

• docs/design-mutual-recursion-lowering.md The R2.1 rewrite cleanly retires the old raw-carrier shape at the design level and keeps the five-Behavior constraint intact.

ROADMAP — Verified

• Lane 3 Stage 3a.1 direction: The docs stay aligned on lowering mutual recursion through Loop instead of drifting back to the rejected lens-level SCC design.

ROADMAP — Incomplete

• Track 9 substrate integrity primitives graduation: The ledger is ahead of the substrate authority: the primitives are present, but their advertised first consumers are not yet reflected in src/v3/std/substrate.dag.

⚠️ The modeling direction is right, but this PR currently records Track 9 as graduated before the substrate authority actually uses the new carriers.

[briansrls]

This is the substrate integrity primitives graduation we discussed at the cross-PR level — the structural answer to the "lossy compression at substrate" class that surfaced in #511, #513, and #515 review loops. Doc PR (ROADMAP + design-mutual-recursion-lowering.md), CI green, mergeable.

Anchored in INVARIANTS.md L:992 ("every fact in one place") and L:2022 ("make illegal states unrepresentable").

Structural assessment — right move

Picks "tighten with reusable primitives" over "dissolve specific records" (the alternative I'd floated on #511). The primitive route is arguably cleaner because the carriers are reusable: TransformRef is the next typed-NodeId story, NonSingletonList is the next "binary-relation carrier" story, ArityIndex is the next index-into-arity-bearing-thing. Not bespoke for DB-9.

Strengths worth banking:

• Replaces "enforced by construction" dissolution receipts with type-level ones — exactly what the prior round's review found missing.
• Names a planned second consumer (IndexedElement<T>.index in std/list.dag) — proves the primitives are general, not single-use.
• Rejected Dag.nodes: List<Behavior> → per-kind lists explicitly with reasoning ("Rust-side consumer migration is independent of this doc-level graduation; file separately when a consumer benefits"). That's graduation discipline, not scope creep.
• Closes the cross-PR class as a Track 9 ledger entry instead of a feedback memo — the right home for an invariant that lives in the substrate vocabulary.

Codex blocker — labeling, not structural

Codex says "primitive declarations landed without the matching consumer-side substrate migration → either land the actual hookup or rewrite as planned future consumers."

But the doc DOES already mark this as design-only:

• ROADMAP entry status: 🟡 Design
• ROADMAP entry text: "Declarations land in src/v3/std/substrate.dag with the DB-9 Lane 3 Stage 3a.1 implementation PR (same commit as the first consumers — the primitives without consumers would be decorative)."

So codex's prescription "land OR rewrite as planned" is already satisfied by the second branch. The misread is probably driven by:

1. Section header "substrate integrity primitives graduation" (reads past-tense)
2. Changelog line "R2.1 approved" (reads landed)
3. Status badge "🟡 Design" without the explicit "no code yet" qualifier

Recommended tightening (5-10 line doc edit)

1. Track 9 section header — add scope qualifier:

   **Surfaced by PR #511 review loop (2026-04-17) — substrate integrity
   primitives graduation (design only; declarations land with DB-9 impl PR):**
   

2. One leading sentence under the table to set expectation before any reader scans into details:

   This entry is a design ledger; the primitive declarations have not been
   written to `src/v3/std/substrate.dag` yet — they land alongside their
   first consumers in the DB-9 Lane 3 Stage 3a.1 implementation PR.
   

3. Status line — bolder:

   **Status:** 🟡 Design only — no `substrate.dag` changes in this PR.
   Declarations land alongside first consumers in the DB-9 implementation PR.
   

4. Changelog R2.1 entry — one word change:

   - **2026-04-17 R2.1 (design)** — graduated substrate records onto Track 9...
   

No structural change. Just makes the design-vs-landed boundary impossible to misread.

Verdict

APPROVE after the labeling tightening. The codex blocker is mechanical; structurally this is exactly the right close for the cross-PR pattern. Once landed, this also unblocks the DB-9 Lane 3 Stage 3a.1 impl PR with a much stronger contract — the impl PR can simply land the primitives + consumers as one structurally-honest substrate addition, rather than re-litigating shape decisions.

[briansrls]

ChatGPT Review

Principle audit.

1. FAIL-CLOSED. Satisfied. For a docs-only round, this is in good shape: the new story is “opaque typed handle with a fail-closed constructor,” not “raw Int/NodeId plus trust the producer.” I do not see a new silent-success path being normalized here.

2. ILLEGAL STATES UNREPRESENTABLE. Satisfied, and this is the big win in the round. The earlier ArityIndex problem is genuinely gone: NonEmptyList<T>, NonSingletonList<T>, ParamRef, and TransformRef move the key invalid states onto the shape instead of leaving them in constructor prose. That matches both the thesis’s decompression direction and the discipline’s “illegal states unrepresentable” bar.

3. FACTS FLOW FORWARD. BLOCKING. The storage shape is improved, but one consumer paragraph now seems semantically inconsistent with the fact it just preserved. The doc explicitly says mixed-position SCCs are real and that MemberDescent.param is per-member to capture them (docs/design-mutual-recursion-lowering.md, diff lines 138-139). But the termination-lens paragraph then says the lens should verify “the argument at the caller-member’s descent slot” against “the caller’s parameter at the same slot” (docs/design-mutual-recursion-lowering.md, diff lines 178-179). That drops the callee-side slot fact the new ParamRef carrier was introduced to preserve. If caller and callee descend on different positions, the consumer as written checks the wrong argument slot. I think the lens needs to say it resolves both members’ ParamRefs and compares the argument feeding the callee’s descent param against the caller’s descent param.

4. COPRODUCT DISSOLUTION. Satisfied. No new substrate enum is being added here, and the round actually improves the decomposition story by explicitly demoting ArityIndex from “primitive” to “at most an input to a constructor.” That is the right use of the Track 9 lens.

5. SINGLE AUTHORITY. Satisfied. Transform remains the authoritative callsite; ParamRef becomes the authoritative member/slot relation instead of re-storing (member, position) as parallel facts. I do not see a new second source of truth introduced in the diff.

6. API-LEVEL ENFORCEMENT. Mostly satisfied. The invalid-record problem is much better now: the type shape blocks the old empty/singleton/out-of-arity/mis-kinded states. My only reservation is the same one as #3: the API now gives you the right handles, but the consumer prose still needs to use both handles correctly or it semantically collapses back toward a single-slot rule.

Design question. Is the descent check keyed by the caller’s chosen parameter, the callee’s chosen parameter, or the ordered pair of both? That is the crux, because ParamRef only earns its keep if the lens compares the argument passed into the callee’s designated descent param against the caller’s designated descent param; otherwise heterogeneous per-member measures are still being flattened in consumer logic.

Verdict. REQUEST_CHANGES. This is materially better than the earlier draft, and I think the ParamRef replacement is the right fix for the prior blocker. But I would correct the termination-lens paragraph before merging, because right now the doc says mixed-position SCCs are supported while the consumer prose appears to validate only caller-aligned positions.

LOOP HEALTH: converging — this round cleanly closes the earlier ArityIndex overclaim and makes honest forward progress on Track 9, but one last consumer-side wording fix is needed so the new carrier is consumed with the generality the doc claims.

---

View conversation

[briansrls]

Meta-review in progress... (view conversation)

Loop-health check: is this review cycle making forward progress, or shifting debt? Posts in ~5-15 minutes.

[briansrls]

ChatGPT review in progress... (view conversation)

Check back in ~30 minutes for the full review.