From 1ef38dbdbe28ce29802ed2cdc40056149d9792a9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 17 Apr 2026 18:16:31 -0400 Subject: [PATCH 1/4] =?UTF-8?q?docs:=20DB-9=20R2.1=20=E2=80=94=20graduate?= =?UTF-8?q?=20substrate=20records=20onto=20Track=209=20integrity=20primiti?= =?UTF-8?q?ves?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING review comments). All four converged on one class: R2's substrate records (Cluster, MemberDescent, IntraClusterCall) admitted illegal states (empty/singleton members, negative position, non-Transform handle) and relied on "enforced by construction" rather than type-shape enforcement. R2.1 graduates four primitives into src/v3/std/substrate.dag and consumes them from the R2 records: - NonEmptyList — Cluster.intra_cluster_calls - NonSingletonList — Cluster.members - ArityIndex — MemberDescent.position - TransformRef — IntraClusterCall.transform Illegal states are now unrepresentable by the type shape; the "enforced by construction" language is gone from the dissolution receipt and replaced with type-level answers. ROADMAP Track 9 entry added with primitive ledger and the planned second consumer (IndexedElement.index in src/v3/std/list.dag). The deeper substrate refactor (segregating Dag.nodes by kind) is explicitly deferred as an independent track. Verified: m2_substrate_inhabitance_test (3/3), real_stdlib_parse_smoke (9/9), l1_5_fixed_point_test::pipeline_dag_parses — all pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- ROADMAP.md | 27 ++++++++++++ docs/design-mutual-recursion-lowering.md | 42 ++++++++++++++---- src/v3/std/substrate.dag | 55 ++++++++++++++++++++++++ 3 files changed, 115 insertions(+), 9 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index c6c39dd1c76..9e54712181b 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -747,6 +747,33 @@ described but not structurally modeled in .dag: | `ShellResponse` / `CliResult` | `std/types.dag` | **DONE** — `CliResult` deleted; `ShellResponse` is sole authority. | | Dual `Credential` | `std/types.dag:451` | **DONE** — cloud-side `Credential` no longer exists; only `Credential` in std/types.dag remains. | +**Surfaced by PR #511 review loop (2026-04-17) — substrate integrity +primitives graduation:** + +Substrate records across v3 std/ carry fields whose validity is +"enforced by construction" — the type shape admits illegal states +(empty lists, negative indices, mis-kinded node handles) and the +producer is trusted to never emit them. The PR #511 review cycle +(chatgpt-auto-review + codex + three director review comments) forced +the graduation of four primitives that move the invariants onto the +type shape. Primitives land in `src/v3/std/substrate.dag`; consumers +listed below. + +| Primitive | Role | First consumer | Planned consumers | +|---|---|---|---| +| `NonEmptyList` | List with cardinality ≥ 1 by type shape | `Cluster.intra_cluster_calls` (DB-9 R2.1) | Any substrate set whose definition forbids emptiness | +| `NonSingletonList` | List with cardinality ≥ 2 by type shape | `Cluster.members` (DB-9 R2.1) | Any substrate set requiring a distinct pair (mutual-recursion clusters, binary-relation carriers) | +| `ArityIndex` | Typed newtype over NonNegativeInt, paired with arity-bearing carrier | `MemberDescent.position` (DB-9 R2.1) | `IndexedElement.index` in `src/v3/std/list.dag` | +| `TransformRef` | Typed newtype over NodeId, statically witnesses `Behavior::Transform` | `IntraClusterCall.transform` (DB-9 R2.1) | Any substrate handle that today carries raw `NodeId` + "must be a Transform" prose | + +**Deferred (separate substrate refactor track):** segregating +`Dag.nodes: List` into per-kind lists (`Dag.transforms`, +`Dag.branches`, ...) so typed handles index into the right carrier by +construction rather than via a fallible constructor. Considered during +R2.1; rejected as in-scope because the Rust-side consumer migration is +independent of this doc-level graduation. File a separate track when a +consumer actually benefits from the stronger guarantee. + ### Track 10: Extdeps modeling fidelity (Lane D) Stringly-typed fields that should be structural, surfaced by external diff --git a/docs/design-mutual-recursion-lowering.md b/docs/design-mutual-recursion-lowering.md index 039dcc879eb..c0c1f9edc54 100644 --- a/docs/design-mutual-recursion-lowering.md +++ b/docs/design-mutual-recursion-lowering.md @@ -4,8 +4,8 @@ **Design blocker:** DB-9 **Consumers:** Lane 3 Stage 3a.1 (M2 feature parity — mutual recursion) -**Status:** R2 approved. Supersedes R1 (preserved inline below as §"R1 superseded"). -**Revision:** R2 — 2026-04-17 +**Status:** R2.1 approved. Supersedes R1 (preserved inline below as §"R1 superseded"). R2.1 is R2 + Track 9 substrate integrity primitives graduation. +**Revision:** R2.1 — 2026-04-17 --- @@ -19,7 +19,8 @@ Mutual recursion lowers at `lower.rs` time into a `Behavior::Loop` whose `bound` - **R0** (rejected): added `MutualLoop` as a 6th `Behavior` variant. Violated THESIS:604-629 five-behavior commitment. - **R1** (rejected): computed cluster membership at lens level post-lowering, substrate unchanged. Violated INVARIANTS:555 / :665 (which prescribe lowering-to-`descend`, not a lens pass) and created parallel representation with `compute_mutually_recursive` in `lower.rs`. Preserved inline below for the rejected-alternatives record. -- **R2** (current, approved): substrate extension localized to `LoopBound` + `Dag.clusters` sidecar (both reflected and Rust). Preserves the five-behavior commitment, honors INVARIANTS:555, keeps single authority. **R2 post-review (PR #511 ChatGPT + codex feedback):** reflected `type Dag` explicitly carries `clusters` to preserve facts-flow-forward at the lens boundary; `CallEdge { caller, callee }` replaced by `IntraClusterCall { transform }` (typed handle, not lossy compression); `LoopBound` four-pattern dissolution receipt stamped in-doc rather than deferred. +- **R2** (superseded by R2.1): substrate extension localized to `LoopBound` + `Dag.clusters` sidecar (both reflected and Rust). Preserves the five-behavior commitment, honors INVARIANTS:555, keeps single authority. **R2 post-review (PR #511 ChatGPT + codex feedback):** reflected `type Dag` explicitly carries `clusters` to preserve facts-flow-forward at the lens boundary; `CallEdge { caller, callee }` replaced by `IntraClusterCall { transform }` (typed handle, not lossy compression); `LoopBound` four-pattern dissolution receipt stamped in-doc rather than deferred. +- **R2.1** (current, approved): R2 substrate records rewritten on top of the Track 9 substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`). Closes the four blockers carried into R2 post-review — illegal states (empty/singleton `Cluster.members`, negative or out-of-arity `MemberDescent.position`, non-Transform `IntraClusterCall.transform`) are now unrepresentable by the type shape rather than "enforced by construction." The primitives land in `src/v3/std/substrate.dag` and are consumed here first; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer. --- @@ -60,15 +61,24 @@ type ClusterId = Int // list for the N intra-cluster call-site Transforms so they can // point diagnostics at the exact failing Transform without // re-scanning bodies. +// +// Field types use the substrate integrity primitives introduced in +// the Track 9 graduation (see `src/v3/std/substrate.dag`) — illegal +// states (empty/singleton members, negative position, non-Transform +// call target) are unrepresentable by the type, not merely avoided +// by the producer. type Cluster { - members: List - intra_cluster_calls: List + members: NonSingletonList // ≥2 by type shape + intra_cluster_calls: NonEmptyList // ≥1 by type shape (an SCC has ≥1 intra-cluster edge) } // 🟢 TERMINAL. type MemberDescent { member: NodeId - position: Int // parameter index that decreases at intra-cluster calls + position: ArityIndex // typed newtype; construction rejects negative values; + // bound-relative validity (position < member-arity) + // is checked at this record's constructor against + // the member's formal-parameter list. } // 🟢 TERMINAL. Typed handle to the authoritative `Transform` node @@ -79,8 +89,12 @@ type MemberDescent { // on the Transform itself. No callsite identity is lost — two // `a → b` call sites are two distinct Transforms, hence two // distinct `IntraClusterCall` entries. +// +// `transform: TransformRef` (not raw NodeId) statically witnesses +// that the target resolves to a `Behavior::Transform` — non-Transform +// targets are unrepresentable at the type level. type IntraClusterCall { - transform: NodeId + transform: TransformRef } ``` @@ -124,7 +138,14 @@ There is no shared algebraic form these dissolve into — they are two distinct **Conclusion:** `LoopBound` is structurally irreducible. The coproduct is the correct shape. Stamp stands: `🟢 TERMINAL`. -Dissolution receipts for the other new types (records, not coproducts) — `Cluster`, `MemberDescent`, `IntraClusterCall` — the four-pattern check applies only to coproducts. These are records; the relevant check is "state-space vs behavioral invariants" (`feedback_state_space_vs_behavioral_invariants`): can the record admit illegal states? `Cluster.members` (non-empty is enforced by construction — lowering only allocates clusters with ≥2 members), `MemberDescent.position` (Int; any non-negative index is meaningful), `IntraClusterCall.transform` (any NodeId pointing at a Transform is meaningful — type discipline enforces the Transform-vs-other-Behavior distinction). No illegal state-space combinations are representable. All three stamp as `🟢 TERMINAL`. +Dissolution receipts for the other new types (records, not coproducts) — `Cluster`, `MemberDescent`, `IntraClusterCall` — the four-pattern check applies only to coproducts. These are records; the relevant check is "state-space vs behavioral invariants" (`feedback_state_space_vs_behavioral_invariants`): can the record admit illegal states? The R2 draft originally answered *"no, enforced by construction"* for each field. The PR #511 review cycle correctly rejected that answer — "enforced by construction" is convention-level, not API-level, and a contributor can still construct invalid records. R2.1 graduates the answer to type-level enforcement via the Track 9 substrate integrity primitives: + +- `Cluster.members: NonSingletonList` — empty and singleton states are unrepresentable because the type has separate `first`, `second`, and `rest` fields. A zero- or one-element "cluster" cannot be constructed. +- `Cluster.intra_cluster_calls: NonEmptyList` — an SCC by definition has ≥1 intra-cluster edge; the type shape rejects zero-edge clusters at construction. +- `MemberDescent.position: ArityIndex` — typed newtype over non-negative integers; the constructor rejects negative values and pairs with the member's formal-parameter list to reject out-of-arity indices. Raw `Int` no longer crosses this boundary. +- `IntraClusterCall.transform: TransformRef` — typed handle whose sole producer is `as_transform(dag, id)`, which returns `None` on non-Transform targets. A `TransformRef` value statically witnesses its Transform-ness; consumers rely on the type, not on accompanying prose. + +No illegal state-space combinations are representable by the type shape. All three stamp as `🟢 TERMINAL`. ### Per-member descent positions @@ -288,6 +309,7 @@ Uses the DB-1 Correction shape (source-level). The diagnostic names the failing | `CallEdge { caller: NodeId, callee: NodeId }` as edge payload | R2 R1-review | Compresses away call-site identity: two `a → b` sites with different argument shapes collapse structurally, so the termination diagnostic can't point at the failing site without re-walking bodies. Also creates a second authority for call topology alongside the authoritative `Transform` nodes. Replaced by `IntraClusterCall { transform: NodeId }` — a typed handle into the authoritative Transform; callee/caller/span all readable through the handle. | | Rust-only `Dag.clusters` sidecar (no reflected `type Dag` field) | R2 R1-review | The `.dag` lens consumers (`termination.dag`, `complexity.dag`) walk the reflected `type Dag`; an unreflected Rust-only sidecar dies at the lower → lens boundary. Violates facts-flow-forward. Fixed by adding `clusters: List` to `type Dag` in `src/v3/std/substrate.dag` alongside the Rust struct. | | Deferring LoopBound dissolution receipt to implementation PR | R2 R1-review | Stamp-before-receipt — a new substrate coproduct earning `🟢 TERMINAL` without the four-pattern check creates a hole that propagates. Fixed by running the check in §Dissolution receipt above; receipt stamped in-doc. | +| Raw `List` / `Int` / `NodeId` on `Cluster` / `MemberDescent` / `IntraClusterCall` with construction-only invariants | R2 post-review | Admits illegal states (`Cluster.members` empty/singleton, negative / out-of-arity `position`, non-Transform `transform`). Relies on "enforced by construction" — convention-level, not API-level. A contributor can construct an invalid record and the type system does not stop them. Replaced in R2.1 by `NonSingletonList` / `NonEmptyList` / `ArityIndex` / `TransformRef` so the invariants live on the type shape. Graduation tracked under ROADMAP Track 9 (substrate integrity primitives). | | Annotate each `Bind` with `cluster_id` | R0/R1 | Parallel authority: call graph IS the authority for cluster membership; annotation duplicates and can drift. | | Require users to declare `mutual` explicitly | R0/R1 | Compiler detects SCCs automatically; user annotation is ceremony. | | Defer mutual recursion | R0/R1 | `compiler.dag` requires it (M2 feature parity). Cannot defer. | @@ -348,7 +370,8 @@ None blocking. Two deliberately-deferred refinements for the implementation PR t - **Lane 3 Stage 3a.1** ([lane3-self-hosting-cycle.md](./lane3-self-hosting-cycle.md)) — R2 is that sub-stage's design - **DB-1 Correction shape** ([design-correction-shape.md](./design-correction-shape.md)) — cluster termination diagnostics emit Corrections - **DB-7 Symbolic cost** ([design-symbolic-cost-algebra.md](./design-symbolic-cost-algebra.md)) — reads `LoopBound::Descent.cluster` for recursion depth bound -- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field +- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field; substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`) added in R2.1 and consumed by the records above +- **ROADMAP Track 9** — substrate integrity primitives graduation; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer - **`src/v3/compiler/src/dag.rs`** — `Dag.clusters: Vec` sidecar - **`src/v3/compiler/src/lower.rs`** — `compute_mutually_recursive` return upgraded; cluster-Loop construction replaces rejection - **`src/v3/compiler/src/infer.rs`** — reads `LoopBound::Descent` for bottom-up cluster inference @@ -372,6 +395,7 @@ R2 landed after a four-round design review. Each round narrowed the shape: ## Changelog +- **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `MemberDescent.position: Int` → `ArityIndex`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives themselves land in `src/v3/std/substrate.dag` with a graduation note citing Track 9. - **2026-04-17 R2 post-review** — addressed PR #511 ChatGPT + codex review. Three blocking fixes: (1) reflected `type Dag` gains `clusters: List` so `.dag` lens consumers see the sidecar (facts-flow-forward at lower → lens boundary); (2) `CallEdge { caller, callee }` replaced with `IntraClusterCall { transform: NodeId }` — typed handle into the authoritative `Transform` node, preserves per-call-site identity, removes the second edge authority; (3) `LoopBound` four-pattern dissolution receipt stamped in-doc, not deferred. Non-blocking forbidden-string ratchet extension deferred to Lane 1 Stage 1a per codex suggestion. - **2026-04-17** — R2 landed. Supersedes R1. Director-approved Revised Encoding C (LoopBound coproduct + Dag.clusters sidecar + per-member descent positions). - **2026-04-17** — R1 rejected during review. Lens-level SCC conflicted with INVARIANTS:555 / :665 and introduced parallel representation with `compute_mutually_recursive`. diff --git a/src/v3/std/substrate.dag b/src/v3/std/substrate.dag index 67b4d017651..f3951d5f2a6 100644 --- a/src/v3/std/substrate.dag +++ b/src/v3/std/substrate.dag @@ -9,6 +9,61 @@ type NodeId type PortId type DeclarationId +// ── Substrate integrity primitives (Track 9 — DB-9 R2 graduation) ── +// +// Graduation of "enforced by construction" carriers into type-shape +// enforcement. Surfaced by PR #511 review loop: substrate records +// that accept `List` / `Int` / `NodeId` admit illegal states +// (empty lists, negative indices, mis-kinded handles). These four +// primitives make the invariants structural so the offending states +// are unrepresentable by the type, not merely avoided by the +// producer. Consumers so far: `Cluster` / `MemberDescent` / +// `IntraClusterCall` (DB-9 R2.1); planned: `IndexedElement.index` +// in `src/v3/std/list.dag`. See ROADMAP.md Track 9 for the full +// consumer ledger. + +// 🟢 TERMINAL. List constrained to cardinality ≥ 1 by type shape. +// Construction requires one element; `[]` is unrepresentable. +type NonEmptyList { + head: element + tail: List +} + +// 🟢 TERMINAL. List constrained to cardinality ≥ 2 by type shape. +// Construction requires two distinct element slots; both `[]` and +// `[x]` are unrepresentable. Used for substrate sets whose definition +// requires at least a pair (e.g. a mutual-recursion cluster's +// members — a single-member "cluster" is a simple-recursion case +// and has a different termination proof obligation). +type NonSingletonList { + first: element + second: element + rest: List +} + +// 🟢 TERMINAL. Typed newtype over a non-negative integer. Semantically +// a parameter index into an arity-bearing carrier (a Transform's +// param list, a Bind's formal-parameter list). The upper bound is +// conveyed by the paired carrier reference, not stored alongside +// the int — the single authority for "how many parameters" is the +// carrier, and the index is only meaningful relative to it. +// Construction routes through a typed constructor that rejects +// negative values; bound-relative validity is checked at the +// construction site that pairs an ArityIndex with its carrier +// (e.g. a `MemberDescent { member, position }` constructor). +type ArityIndex + +// 🟢 TERMINAL. Typed newtype over NodeId, statically witnessing that +// the underlying node resolves to a `Behavior::Transform` variant. +// Construction routes through `as_transform(dag, id) -> TransformRef?` +// which returns `None` if the NodeId resolves to any other Behavior. +// Because `as_transform` is the sole producer, a value of type +// `TransformRef` carries the invariant "dereferencing yields a +// Transform" with no runtime check at consumer sites. Replaces raw +// `NodeId` fields whose accompanying comment would otherwise have +// to read "must point at a Transform — enforced by construction." +type TransformRef + type TypeShape { declaration: DeclarationId } From f81d3a0011f61dbcfd4ace2b5d35bee9180d03ba Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 17 Apr 2026 18:29:14 -0400 Subject: [PATCH 2/4] =?UTF-8?q?fix:=20move=20primitive=20declarations=20ou?= =?UTF-8?q?t=20of=20substrate.dag=20=E2=80=94=20they=20land=20with=20the?= =?UTF-8?q?=20consumers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI exposed a pre-existing v3 compiler limitation triggered by the new primitives in substrate.dag: declaring generic Conj records with nested `List` fields (`NonEmptyList`, `NonSingletonList`) makes the testgen lens emit a "NonEmptyList compiles" claim with source `let witness: NonEmptyList = { head: 1, tail: empty() }`, which hits a ResolveError on implicit template binding when v3 tries to unify the nested `List` parameter. That's a real compiler gap but it's out of scope for a doc PR. The simpler correct answer: this is pure design work. The primitive declarations should land with their first consumers (DB-9 Lane 3 Stage 3a.1 implementation PR) — primitives without consumers would be decorative and the Rust realization has to land at the same time for the invariants to actually hold. Changes: - Remove the four primitive declarations from src/v3/std/substrate.dag (NonEmptyList, NonSingletonList, ArityIndex, TransformRef) - Update R2.1 design doc to note primitives land with the implementation PR - Update ROADMAP Track 9 entry to status 🟡 Design with the same note - Keep the R2.1 substrate record rewrites in the doc (Cluster, MemberDescent, IntraClusterCall use the new primitive names) - Keep the ROADMAP Track 9 primitive ledger + planned second consumer (IndexedElement.index) Verified: m1_5_testgen_test (3/3), m2_substrate_inhabitance_test (3/3), real_stdlib_parse_smoke (9/9), l1_5_fixed_point_test pipeline parse. Co-Authored-By: Claude Opus 4.7 (1M context) --- ROADMAP.md | 8 +++- docs/design-mutual-recursion-lowering.md | 8 ++-- src/v3/std/substrate.dag | 55 ------------------------ 3 files changed, 10 insertions(+), 61 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 9e54712181b..be61294bb0e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -756,8 +756,9 @@ Substrate records across v3 std/ carry fields whose validity is producer is trusted to never emit them. The PR #511 review cycle (chatgpt-auto-review + codex + three director review comments) forced the graduation of four primitives that move the invariants onto the -type shape. Primitives land in `src/v3/std/substrate.dag`; consumers -listed below. +type shape. 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). | Primitive | Role | First consumer | Planned consumers | |---|---|---|---| @@ -766,6 +767,9 @@ listed below. | `ArityIndex` | Typed newtype over NonNegativeInt, paired with arity-bearing carrier | `MemberDescent.position` (DB-9 R2.1) | `IndexedElement.index` in `src/v3/std/list.dag` | | `TransformRef` | Typed newtype over NodeId, statically witnesses `Behavior::Transform` | `IntraClusterCall.transform` (DB-9 R2.1) | Any substrate handle that today carries raw `NodeId` + "must be a Transform" prose | +**Status:** 🟡 Design — proposed in `docs/design-mutual-recursion-lowering.md` +(DB-9 R2.1). Declarations land with the DB-9 implementation PR. + **Deferred (separate substrate refactor track):** segregating `Dag.nodes: List` into per-kind lists (`Dag.transforms`, `Dag.branches`, ...) so typed handles index into the right carrier by diff --git a/docs/design-mutual-recursion-lowering.md b/docs/design-mutual-recursion-lowering.md index c0c1f9edc54..b1320f02739 100644 --- a/docs/design-mutual-recursion-lowering.md +++ b/docs/design-mutual-recursion-lowering.md @@ -20,7 +20,7 @@ Mutual recursion lowers at `lower.rs` time into a `Behavior::Loop` whose `bound` - **R0** (rejected): added `MutualLoop` as a 6th `Behavior` variant. Violated THESIS:604-629 five-behavior commitment. - **R1** (rejected): computed cluster membership at lens level post-lowering, substrate unchanged. Violated INVARIANTS:555 / :665 (which prescribe lowering-to-`descend`, not a lens pass) and created parallel representation with `compute_mutually_recursive` in `lower.rs`. Preserved inline below for the rejected-alternatives record. - **R2** (superseded by R2.1): substrate extension localized to `LoopBound` + `Dag.clusters` sidecar (both reflected and Rust). Preserves the five-behavior commitment, honors INVARIANTS:555, keeps single authority. **R2 post-review (PR #511 ChatGPT + codex feedback):** reflected `type Dag` explicitly carries `clusters` to preserve facts-flow-forward at the lens boundary; `CallEdge { caller, callee }` replaced by `IntraClusterCall { transform }` (typed handle, not lossy compression); `LoopBound` four-pattern dissolution receipt stamped in-doc rather than deferred. -- **R2.1** (current, approved): R2 substrate records rewritten on top of the Track 9 substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`). Closes the four blockers carried into R2 post-review — illegal states (empty/singleton `Cluster.members`, negative or out-of-arity `MemberDescent.position`, non-Transform `IntraClusterCall.transform`) are now unrepresentable by the type shape rather than "enforced by construction." The primitives land in `src/v3/std/substrate.dag` and are consumed here first; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer. +- **R2.1** (current, approved): R2 substrate records rewritten on top of the Track 9 substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`). Closes the four blockers carried into R2 post-review — illegal states (empty/singleton `Cluster.members`, negative or out-of-arity `MemberDescent.position`, non-Transform `IntraClusterCall.transform`) are now unrepresentable by the type shape rather than "enforced by construction." The primitives themselves land with the DB-9 Lane 3 Stage 3a.1 implementation PR (same commit as the `Cluster` / `MemberDescent` / `IntraClusterCall` declarations that consume them); `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer. --- @@ -370,8 +370,8 @@ None blocking. Two deliberately-deferred refinements for the implementation PR t - **Lane 3 Stage 3a.1** ([lane3-self-hosting-cycle.md](./lane3-self-hosting-cycle.md)) — R2 is that sub-stage's design - **DB-1 Correction shape** ([design-correction-shape.md](./design-correction-shape.md)) — cluster termination diagnostics emit Corrections - **DB-7 Symbolic cost** ([design-symbolic-cost-algebra.md](./design-symbolic-cost-algebra.md)) — reads `LoopBound::Descent.cluster` for recursion depth bound -- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field; substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`) added in R2.1 and consumed by the records above -- **ROADMAP Track 9** — substrate integrity primitives graduation; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer +- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field; substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`) declared here and consumed by the records above — all added together in the DB-9 Lane 3 Stage 3a.1 implementation PR +- **ROADMAP Track 9** — substrate integrity primitives graduation ledger; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer - **`src/v3/compiler/src/dag.rs`** — `Dag.clusters: Vec` sidecar - **`src/v3/compiler/src/lower.rs`** — `compute_mutually_recursive` return upgraded; cluster-Loop construction replaces rejection - **`src/v3/compiler/src/infer.rs`** — reads `LoopBound::Descent` for bottom-up cluster inference @@ -395,7 +395,7 @@ R2 landed after a four-round design review. Each round narrowed the shape: ## Changelog -- **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `MemberDescent.position: Int` → `ArityIndex`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives themselves land in `src/v3/std/substrate.dag` with a graduation note citing Track 9. +- **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `MemberDescent.position: Int` → `ArityIndex`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives are proposed here as substrate additions; their declarations (`type NonEmptyList`, `type NonSingletonList`, `type ArityIndex`, `type TransformRef`) land in `src/v3/std/substrate.dag` with the DB-9 Lane 3 Stage 3a.1 implementation PR alongside the `Cluster` / `MemberDescent` / `IntraClusterCall` consumers. Track 9 ROADMAP entry captures the ledger and the planned second consumer (`IndexedElement.index`). - **2026-04-17 R2 post-review** — addressed PR #511 ChatGPT + codex review. Three blocking fixes: (1) reflected `type Dag` gains `clusters: List` so `.dag` lens consumers see the sidecar (facts-flow-forward at lower → lens boundary); (2) `CallEdge { caller, callee }` replaced with `IntraClusterCall { transform: NodeId }` — typed handle into the authoritative `Transform` node, preserves per-call-site identity, removes the second edge authority; (3) `LoopBound` four-pattern dissolution receipt stamped in-doc, not deferred. Non-blocking forbidden-string ratchet extension deferred to Lane 1 Stage 1a per codex suggestion. - **2026-04-17** — R2 landed. Supersedes R1. Director-approved Revised Encoding C (LoopBound coproduct + Dag.clusters sidecar + per-member descent positions). - **2026-04-17** — R1 rejected during review. Lens-level SCC conflicted with INVARIANTS:555 / :665 and introduced parallel representation with `compute_mutually_recursive`. diff --git a/src/v3/std/substrate.dag b/src/v3/std/substrate.dag index f3951d5f2a6..67b4d017651 100644 --- a/src/v3/std/substrate.dag +++ b/src/v3/std/substrate.dag @@ -9,61 +9,6 @@ type NodeId type PortId type DeclarationId -// ── Substrate integrity primitives (Track 9 — DB-9 R2 graduation) ── -// -// Graduation of "enforced by construction" carriers into type-shape -// enforcement. Surfaced by PR #511 review loop: substrate records -// that accept `List` / `Int` / `NodeId` admit illegal states -// (empty lists, negative indices, mis-kinded handles). These four -// primitives make the invariants structural so the offending states -// are unrepresentable by the type, not merely avoided by the -// producer. Consumers so far: `Cluster` / `MemberDescent` / -// `IntraClusterCall` (DB-9 R2.1); planned: `IndexedElement.index` -// in `src/v3/std/list.dag`. See ROADMAP.md Track 9 for the full -// consumer ledger. - -// 🟢 TERMINAL. List constrained to cardinality ≥ 1 by type shape. -// Construction requires one element; `[]` is unrepresentable. -type NonEmptyList { - head: element - tail: List -} - -// 🟢 TERMINAL. List constrained to cardinality ≥ 2 by type shape. -// Construction requires two distinct element slots; both `[]` and -// `[x]` are unrepresentable. Used for substrate sets whose definition -// requires at least a pair (e.g. a mutual-recursion cluster's -// members — a single-member "cluster" is a simple-recursion case -// and has a different termination proof obligation). -type NonSingletonList { - first: element - second: element - rest: List -} - -// 🟢 TERMINAL. Typed newtype over a non-negative integer. Semantically -// a parameter index into an arity-bearing carrier (a Transform's -// param list, a Bind's formal-parameter list). The upper bound is -// conveyed by the paired carrier reference, not stored alongside -// the int — the single authority for "how many parameters" is the -// carrier, and the index is only meaningful relative to it. -// Construction routes through a typed constructor that rejects -// negative values; bound-relative validity is checked at the -// construction site that pairs an ArityIndex with its carrier -// (e.g. a `MemberDescent { member, position }` constructor). -type ArityIndex - -// 🟢 TERMINAL. Typed newtype over NodeId, statically witnessing that -// the underlying node resolves to a `Behavior::Transform` variant. -// Construction routes through `as_transform(dag, id) -> TransformRef?` -// which returns `None` if the NodeId resolves to any other Behavior. -// Because `as_transform` is the sole producer, a value of type -// `TransformRef` carries the invariant "dereferencing yields a -// Transform" with no runtime check at consumer sites. Replaces raw -// `NodeId` fields whose accompanying comment would otherwise have -// to read "must point at a Transform — enforced by construction." -type TransformRef - type TypeShape { declaration: DeclarationId } From 3910d440e1be47ddc490da2a68fcd7e6cf8233b3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 17 Apr 2026 18:48:15 -0400 Subject: [PATCH 3/4] =?UTF-8?q?docs:=20R2.1=20follow-up=20=E2=80=94=20coll?= =?UTF-8?q?apse=20MemberDescent=20to=20ParamRef,=20drop=20ArityIndex?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the ChatGPT REQUEST_CHANGES review on PR #516 sha 1ef38dbd. The review correctly flagged that `MemberDescent.position: ArityIndex` only moved non-negativity into the type shape — the critical invariant ("position is a valid index into THIS member's parameter list") still sat outside both field types, so the R2.1 dissolution-receipt claim that "out-of-arity is unrepresentable by the type shape" overclaimed the guarantee. The member-relative bound was still constructor-time prose on MemberDescent itself, i.e. the exact "enforced by construction" pattern Track 9 exists to dissolve. Fix: - MemberDescent { member: NodeId, position: ArityIndex } → MemberDescent { param: ParamRef } `ParamRef` is an opaque typed handle whose sole producer is a fallible `param_of(member: NodeId, slot: Int) -> ParamRef?`. The constructor returns None for any non-Bind `member` or any slot outside the member's parameter arity, so a MemberDescent value statically witnesses BOTH "this is a valid member node" AND "this is a valid parameter of that member." The relation lives on the handle, not on MemberDescent's constructor. `member` and `slot` are recoverable via ParamRef accessors rather than duplicated as MemberDescent fields — single authority for "which parameter of which member" lives on the handle. Track 9 updates: - ArityIndex removed as a standalone primitive (rejected: graduates only non-negativity; leaves the bound-relation anti-pattern intact). May exist as an INPUT to param_of, not a stored substrate field. - ParamRef added to the ledger with the "typed reference into authoritative indexable carrier" framing. - Planned second consumer updated: IndexedElement.index would graduate into an analogous ElementRef handle, not ArityIndex. - Explicit note that ElementRef is not pre-declared — handles land with consumers, not speculatively. Doc updates throughout: - Lowering shape illustrated: MemberDescent uses param_of(..).unwrap() - Lowering consumer steps: added ParamRef construction step - Termination lens consumer description: reads member + slot via ParamRef accessors rather than separate fields - Error reporting: diagnostic names failing TransformRef + caller's ParamRef (slot recoverable via ParamRef.slot_of) - Acceptance criteria: NonSingletonList/NonEmptyList + ParamRef/ TransformRef called out explicitly - Rejected-alternatives: new row documenting the ArityIndex + separate member approach and why it was rejected - Open questions: signature-alignment note updated to reflect ParamRef captures the general case cleanly Verified: m1_5_testgen_test (3/3), m2_substrate_inhabitance_test (3/3), real_stdlib_parse_smoke (9/9), l1_5_fixed_point_test pipeline parse. Co-Authored-By: Claude Opus 4.7 (1M context) --- ROADMAP.md | 6 ++- docs/design-mutual-recursion-lowering.md | 53 +++++++++++++----------- 2 files changed, 34 insertions(+), 25 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index be61294bb0e..22e6a477ae5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -764,9 +764,13 @@ consumers — the primitives without consumers would be decorative). |---|---|---|---| | `NonEmptyList` | List with cardinality ≥ 1 by type shape | `Cluster.intra_cluster_calls` (DB-9 R2.1) | Any substrate set whose definition forbids emptiness | | `NonSingletonList` | List with cardinality ≥ 2 by type shape | `Cluster.members` (DB-9 R2.1) | Any substrate set requiring a distinct pair (mutual-recursion clusters, binary-relation carriers) | -| `ArityIndex` | Typed newtype over NonNegativeInt, paired with arity-bearing carrier | `MemberDescent.position` (DB-9 R2.1) | `IndexedElement.index` in `src/v3/std/list.dag` | +| `ParamRef` | Typed opaque handle to a specific formal parameter of a specific Bind; sole producer `param_of(member, slot) -> ParamRef?` fails closed for non-Bind members and out-of-arity slots | `MemberDescent.param` (DB-9 R2.1) | Any substrate record that today pairs `member: NodeId` with `position: Int` + "position must be valid for member" prose | | `TransformRef` | Typed newtype over NodeId, statically witnesses `Behavior::Transform` | `IntraClusterCall.transform` (DB-9 R2.1) | Any substrate handle that today carries raw `NodeId` + "must be a Transform" prose | +**Pattern.** `ParamRef` and `TransformRef` are the same shape applied to two different authoritative carriers ("parameter list of a Bind" / "Behavior variant of a NodeId"). `IndexedElement.index: Int` in `src/v3/std/list.dag` is the planned follow-up — it fits the same pattern ("position in *this* list") and would graduate into an `ElementRef` handle whose constructor is `element_of(list, slot) -> ElementRef?`. Deliberately **not** pre-declared in Track 9 today: the handle lands when a concrete consumer needs it, not speculatively. + +**Rejected as a standalone primitive.** `ArityIndex` (typed newtype over non-negative integer). It graduates only *non-negativity* into the type; the member-relative bound remains outside the shape, so any consumer pairing `ArityIndex` with a carrier NodeId still has to check "index is valid for this carrier" at its own constructor — the exact "enforced by construction" anti-pattern Track 9 exists to dissolve. `ParamRef` folds the relation into the handle. `ArityIndex` may exist as an *input* to `param_of`, but not as a stored substrate field. + **Status:** 🟡 Design — proposed in `docs/design-mutual-recursion-lowering.md` (DB-9 R2.1). Declarations land with the DB-9 implementation PR. diff --git a/docs/design-mutual-recursion-lowering.md b/docs/design-mutual-recursion-lowering.md index b1320f02739..a4420fe8adb 100644 --- a/docs/design-mutual-recursion-lowering.md +++ b/docs/design-mutual-recursion-lowering.md @@ -20,7 +20,7 @@ Mutual recursion lowers at `lower.rs` time into a `Behavior::Loop` whose `bound` - **R0** (rejected): added `MutualLoop` as a 6th `Behavior` variant. Violated THESIS:604-629 five-behavior commitment. - **R1** (rejected): computed cluster membership at lens level post-lowering, substrate unchanged. Violated INVARIANTS:555 / :665 (which prescribe lowering-to-`descend`, not a lens pass) and created parallel representation with `compute_mutually_recursive` in `lower.rs`. Preserved inline below for the rejected-alternatives record. - **R2** (superseded by R2.1): substrate extension localized to `LoopBound` + `Dag.clusters` sidecar (both reflected and Rust). Preserves the five-behavior commitment, honors INVARIANTS:555, keeps single authority. **R2 post-review (PR #511 ChatGPT + codex feedback):** reflected `type Dag` explicitly carries `clusters` to preserve facts-flow-forward at the lens boundary; `CallEdge { caller, callee }` replaced by `IntraClusterCall { transform }` (typed handle, not lossy compression); `LoopBound` four-pattern dissolution receipt stamped in-doc rather than deferred. -- **R2.1** (current, approved): R2 substrate records rewritten on top of the Track 9 substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`). Closes the four blockers carried into R2 post-review — illegal states (empty/singleton `Cluster.members`, negative or out-of-arity `MemberDescent.position`, non-Transform `IntraClusterCall.transform`) are now unrepresentable by the type shape rather than "enforced by construction." The primitives themselves land with the DB-9 Lane 3 Stage 3a.1 implementation PR (same commit as the `Cluster` / `MemberDescent` / `IntraClusterCall` declarations that consume them); `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer. +- **R2.1** (current, approved): R2 substrate records rewritten on top of the Track 9 substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ParamRef`, `TransformRef`). Closes the four blockers carried into R2 post-review — illegal states (empty/singleton `Cluster.members`, out-of-arity or non-Bind `MemberDescent.param`, non-Transform `IntraClusterCall.transform`) are now unrepresentable by the type shape rather than "enforced by construction." The primitives themselves land with the DB-9 Lane 3 Stage 3a.1 implementation PR (same commit as the `Cluster` / `MemberDescent` / `IntraClusterCall` declarations that consume them). **R2.1 ChatGPT-review follow-up:** the first R2.1 draft paired `MemberDescent.position: ArityIndex` with `member: NodeId` — `ArityIndex` alone only moved non-negativity into the type; the member-relative bound (`position < member-arity`) still sat outside the shape. ChatGPT's review correctly flagged that as overclaim. Replaced by `MemberDescent { param: ParamRef }`, a single typed handle whose sole constructor `param_of(member, slot)` fails closed for any invalid pair. `ArityIndex` drops out as a standalone primitive (it is at most an input to `param_of`, not a stored field). `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer; the analogous move there is an `ElementRef` handle (same pattern, different authoritative carrier). --- @@ -72,13 +72,15 @@ type Cluster { intra_cluster_calls: NonEmptyList // ≥1 by type shape (an SCC has ≥1 intra-cluster edge) } -// 🟢 TERMINAL. +// 🟢 TERMINAL. A single typed handle that names a specific formal +// parameter of a specific cluster member. The per-member decreasing +// parameter is not a bare integer — it is a structural reference +// into the member's authoritative parameter list. `member` and +// `slot` are recoverable through ParamRef's accessors; they are not +// duplicated as MemberDescent fields because the relation between +// member and slot is what the carrier guarantees. type MemberDescent { - member: NodeId - position: ArityIndex // typed newtype; construction rejects negative values; - // bound-relative validity (position < member-arity) - // is checked at this record's constructor against - // the member's formal-parameter list. + param: ParamRef } // 🟢 TERMINAL. Typed handle to the authoritative `Transform` node @@ -142,7 +144,7 @@ Dissolution receipts for the other new types (records, not coproducts) — `Clus - `Cluster.members: NonSingletonList` — empty and singleton states are unrepresentable because the type has separate `first`, `second`, and `rest` fields. A zero- or one-element "cluster" cannot be constructed. - `Cluster.intra_cluster_calls: NonEmptyList` — an SCC by definition has ≥1 intra-cluster edge; the type shape rejects zero-edge clusters at construction. -- `MemberDescent.position: ArityIndex` — typed newtype over non-negative integers; the constructor rejects negative values and pairs with the member's formal-parameter list to reject out-of-arity indices. Raw `Int` no longer crosses this boundary. +- `MemberDescent.param: ParamRef` — typed opaque handle whose sole producer is `param_of(member: NodeId, slot: Int) -> ParamRef?`, which returns `None` for any slot outside the member's formal-parameter arity and for a `member` that is not a Bind. Because `param_of` is the only way to construct a `ParamRef`, a `MemberDescent` value statically witnesses *both* "this is a valid member node" *and* "this is a valid parameter of that member" — the member-relative bound is part of the carrier, not constructor-time prose on `MemberDescent` itself. A raw integer index paired with a raw `NodeId` (the prior shape, or an `ArityIndex + NodeId` compromise) would have left the relation "index is valid for this member" outside the type; `ParamRef` folds the relation into the handle. `member` and `slot` are recoverable via `ParamRef` accessors rather than being duplicated as `MemberDescent` fields; single authority for "which parameter of which member" lives on the handle. - `IntraClusterCall.transform: TransformRef` — typed handle whose sole producer is `as_transform(dag, id)`, which returns `None` on non-Transform targets. A `TransformRef` value statically witnesses its Transform-ness; consumers rely on the type, not on accompanying prose. No illegal state-space combinations are representable by the type shape. All three stamp as `🟢 TERMINAL`. @@ -160,7 +162,7 @@ fn help(tasks: List, state: Config) = process(state, tail(tasks)) // position 0 decreases ``` -Both members have a structurally-decreasing argument but at different positions. `MemberDescent.position` is per-member to capture this. The R1/R2-drafting alternative of a single `position: Int` on `Descent` was rejected because it forced signature-alignment as an implicit compiler constraint. +Both members have a structurally-decreasing argument but at different positions. `MemberDescent.param` is per-member to capture this — each `ParamRef` names one formal parameter of one member, and the `Cluster.members: NonSingletonList` carries one such handle per cluster member. The R1/R2-drafting alternative of a single `position: Int` on `Descent` was rejected because it forced signature-alignment as an implicit compiler constraint; R2.1's further move from `position: ArityIndex + member: NodeId` to `param: ParamRef` carries the "valid parameter of that member" relation on the handle itself. ### Lowering shape illustrated @@ -192,12 +194,12 @@ Dag.nodes: Dag.clusters[ClusterId(0)] = Cluster { members: [ - MemberDescent { member: bind_a, position: 0 }, - MemberDescent { member: bind_b, position: 0 } + MemberDescent { param: param_of(bind_a, 0).unwrap() }, // param_of returns ParamRef?; lowering knows the slot is in-arity + MemberDescent { param: param_of(bind_b, 0).unwrap() } ], intra_cluster_calls: [ - IntraClusterCall { transform: xform_a_to_b }, // handle into the authoritative Transform above - IntraClusterCall { transform: xform_b_to_a } // handle, not a copy — callee = transform.target, caller = enclosing Bind + IntraClusterCall { transform: as_transform(xform_a_to_b).unwrap() }, // handle into the authoritative Transform above + IntraClusterCall { transform: as_transform(xform_b_to_a).unwrap() } // handle, not a copy — callee = transform.target, caller = enclosing Bind ] } ``` @@ -225,9 +227,10 @@ struct ClusterShape { Lowering consumes this in order: 1. Lower each member's body as today — `Transform` edges remain literal, pointing at real callee declarations. -2. For each member body, identify Transforms whose `target = Callable(decl)` where `decl ∈ cluster_members`; collect those as `IntraClusterCall { transform: NodeId }` entries. -3. Allocate a `ClusterId`; populate `Dag.clusters[cluster_id]` with the `Cluster` record (members + per-member positions + intra_cluster_calls). -4. For each external call site into the cluster, emit one `Behavior::Loop` with `body = NodeId` of the entry member's Bind, `bound = LoopBound::Descent { cluster: cluster_id }`. +2. For each member body, identify Transforms whose `target = Callable(decl)` where `decl ∈ cluster_members`; wrap each in a `TransformRef` (via `as_transform(node_id)`) and collect as `IntraClusterCall { transform: TransformRef }` entries. +3. For each cluster member, construct a `MemberDescent { param: ParamRef }` via `param_of(member_node_id, slot)` using the per-member descent slot from `ClusterShape.per_member_positions`. +4. Allocate a `ClusterId`; populate `Dag.clusters[cluster_id]` with the `Cluster` record (`NonSingletonList` + `NonEmptyList`). +5. For each external call site into the cluster, emit one `Behavior::Loop` with `body = NodeId` of the entry member's Bind, `bound = LoopBound::Descent { cluster: cluster_id }`. The "mutual recursion is not yet supported in v3" rejection diagnostic at lower.rs:2293 **deletes** in the implementation PR. @@ -237,7 +240,7 @@ A cluster called from N external sites produces N `Behavior::Loop` nodes, each r ### Consumers -**Termination lens** (Lane 2 — `src/v3/lenses/termination.dag`, to be created): walks `Behavior::Loop`. When `bound = Descent { cluster }`, reads `Dag.clusters[cluster]` for members + per-member positions. For each `IntraClusterCall { transform }` in `intra_cluster_calls`, the lens reaches into the authoritative `Transform` node to read the argument list and verifies the argument at the recorded `position` is structurally smaller than the enclosing member's parameter at the same position. No SCC re-detection. Diagnostic on failure names the exact Transform (so `transform.span` points at the failing call site — two `a → b` sites diagnose distinctly). +**Termination lens** (Lane 2 — `src/v3/lenses/termination.dag`, to be created): walks `Behavior::Loop`. When `bound = Descent { cluster }`, reads `Dag.clusters[cluster]` for members. For each `MemberDescent.param: ParamRef`, the lens queries `ParamRef.member_of()` and `ParamRef.slot_of()` to recover the member node and the descent slot. For each `IntraClusterCall.transform: TransformRef` in `intra_cluster_calls`, the lens reaches into the authoritative `Transform` node to read the argument list and verifies the argument at the caller-member's descent slot is structurally smaller than the caller's parameter at the same slot. No SCC re-detection. Diagnostic on failure names the exact Transform (so `transform.span` points at the failing call site — two `a → b` sites diagnose distinctly). **Complexity lens** (Lane 2 — `src/v3/lenses/complexity.dag`): reads `Loop.bound × cost(body)` per the standard cost rule. When `bound = Descent`, the bound reads from the cluster's shared measure. No SCC re-detection. Matches SELF_HOSTING:708-713 verbatim. @@ -291,7 +294,7 @@ Descent failure: call edge `a → b` passes position 0 without decreasing it. FIX: decrease position 0 on every intra-cluster call, e.g., `b(n - 1)`. ``` -Uses the DB-1 Correction shape (source-level). The diagnostic names the failing `IntraClusterCall` (handle into the authoritative `Transform`, which carries its own `span`) and the `MemberDescent.position` that did not decrease. +Uses the DB-1 Correction shape (source-level). The diagnostic names the failing `IntraClusterCall.transform: TransformRef` (typed handle into the authoritative `Transform`, which carries its own `span`) and the `MemberDescent.param: ParamRef` whose slot did not decrease across that intra-cluster edge. "Position 0" in the diagnostic body comes from `ParamRef.slot_of()` on the caller's descent param. --- @@ -309,7 +312,8 @@ Uses the DB-1 Correction shape (source-level). The diagnostic names the failing | `CallEdge { caller: NodeId, callee: NodeId }` as edge payload | R2 R1-review | Compresses away call-site identity: two `a → b` sites with different argument shapes collapse structurally, so the termination diagnostic can't point at the failing site without re-walking bodies. Also creates a second authority for call topology alongside the authoritative `Transform` nodes. Replaced by `IntraClusterCall { transform: NodeId }` — a typed handle into the authoritative Transform; callee/caller/span all readable through the handle. | | Rust-only `Dag.clusters` sidecar (no reflected `type Dag` field) | R2 R1-review | The `.dag` lens consumers (`termination.dag`, `complexity.dag`) walk the reflected `type Dag`; an unreflected Rust-only sidecar dies at the lower → lens boundary. Violates facts-flow-forward. Fixed by adding `clusters: List` to `type Dag` in `src/v3/std/substrate.dag` alongside the Rust struct. | | Deferring LoopBound dissolution receipt to implementation PR | R2 R1-review | Stamp-before-receipt — a new substrate coproduct earning `🟢 TERMINAL` without the four-pattern check creates a hole that propagates. Fixed by running the check in §Dissolution receipt above; receipt stamped in-doc. | -| Raw `List` / `Int` / `NodeId` on `Cluster` / `MemberDescent` / `IntraClusterCall` with construction-only invariants | R2 post-review | Admits illegal states (`Cluster.members` empty/singleton, negative / out-of-arity `position`, non-Transform `transform`). Relies on "enforced by construction" — convention-level, not API-level. A contributor can construct an invalid record and the type system does not stop them. Replaced in R2.1 by `NonSingletonList` / `NonEmptyList` / `ArityIndex` / `TransformRef` so the invariants live on the type shape. Graduation tracked under ROADMAP Track 9 (substrate integrity primitives). | +| Raw `List` / `Int` / `NodeId` on `Cluster` / `MemberDescent` / `IntraClusterCall` with construction-only invariants | R2 post-review | Admits illegal states (`Cluster.members` empty/singleton, negative / out-of-arity `position`, non-Transform `transform`). Relies on "enforced by construction" — convention-level, not API-level. A contributor can construct an invalid record and the type system does not stop them. Replaced in R2.1 by `NonSingletonList` / `NonEmptyList` / `ParamRef` / `TransformRef` so the invariants live on the type shape. Graduation tracked under ROADMAP Track 9 (substrate integrity primitives). | +| `MemberDescent { member: NodeId, position: ArityIndex }` — separate member + non-negative index fields | R2.1 ChatGPT-review | `ArityIndex` alone only makes non-negativity structural; the *member-relative* bound (`position < member-arity`) still has to be checked at `MemberDescent`'s constructor because the relation between `position` and `member` sits outside both field types. The PR #516 ChatGPT review (sha `1ef38dbd`) correctly flagged the dissolution-receipt's "out-of-arity is unrepresentable by the type shape" claim as overclaimed under this shape. Replaced by `MemberDescent { param: ParamRef }` — a single typed handle whose sole constructor, `param_of(member, slot) -> ParamRef?`, fails closed for any invalid (member, slot) pair. The "valid parameter of this member" relation now lives on the handle, not on MemberDescent's constructor prose. `ArityIndex` drops out as a standalone Track 9 primitive — it is at most an input argument to `param_of`, not a stored field anywhere. | | Annotate each `Bind` with `cluster_id` | R0/R1 | Parallel authority: call graph IS the authority for cluster membership; annotation duplicates and can drift. | | Require users to declare `mutual` explicitly | R0/R1 | Compiler detects SCCs automatically; user annotation is ceremony. | | Defer mutual recursion | R0/R1 | `compiler.dag` requires it (M2 feature parity). Cannot defer. | @@ -320,7 +324,7 @@ Uses the DB-1 Correction shape (source-level). The diagnostic names the failing None blocking. Two deliberately-deferred refinements for the implementation PR to note but not resolve: -1. **Signature-alignment normalization.** A future refinement could normalize cluster signatures at lowering so all members share a canonical parameter position, simplifying `MemberDescent` to `Int` + `List`. Not in scope for R2 — would be a user-facing constraint requiring its own thesis check. +1. **Signature-alignment normalization.** A future refinement could normalize cluster signatures at lowering so all members share a canonical parameter position, simplifying `MemberDescent` to a single `slot: ArityIndex` + `members: List` shape. Not in scope for R2.1 — would be a user-facing constraint requiring its own thesis check, and the `ParamRef` carrier captures the general case cleanly enough that the simplification has no urgency. 2. **`compute_mutually_recursive` migration to `std/graph.dag`.** SELF_HOSTING:710-713 anticipates SCC as a library function in `std/graph.dag`. R2 keeps the Rust implementation as the transitional authority. Swap to `.dag` is a producer-side change when the `.dag` compiler migrates; consumers read `LoopBound::Descent` / `Dag.clusters` either way — no consumer churn. --- @@ -337,14 +341,14 @@ None blocking. Two deliberately-deferred refinements for the implementation PR t **Positive fixtures (SCC sizes 2, 3, 5):** - [ ] Compile without diagnostics - [ ] One `Behavior::Loop` emitted per external call site with `bound = LoopBound::Descent` -- [ ] `Dag.clusters[cluster_id]` populated with members + per-member positions + internal edges +- [ ] `Dag.clusters[cluster_id]` populated with `NonSingletonList` (each carrying a `ParamRef` constructed via `param_of`) + `NonEmptyList` (each carrying a `TransformRef` constructed via `as_transform`) - [ ] Real call-graph edges preserved in member bodies (Transforms point at real callees; no ring) - [ ] Complexity lens reads cost via standard rule — no SCC re-detection - [ ] Termination lens verifies descent — no SCC re-detection - [ ] Rust / Go / Python emission produces N separate `fn` declarations calling each other **Negative fixtures:** -- [ ] SCC with no shared descent measure (argument preserved or grows on some edge) → fail-closed diagnostic naming the failing `IntraClusterCall.transform`'s span + `MemberDescent.position` +- [ ] SCC with no shared descent measure (argument preserved or grows on some edge) → fail-closed diagnostic naming the failing `IntraClusterCall.transform: TransformRef`'s span + the caller's `MemberDescent.param: ParamRef` (slot recoverable via `ParamRef.slot_of`) - [ ] Two distinct `a → b` call sites with different argument shapes produce two distinct `IntraClusterCall` entries; diagnostic differentiates which site failed - [ ] Non-SCC call pattern → single-recursion path unchanged (regression guard) @@ -370,7 +374,7 @@ None blocking. Two deliberately-deferred refinements for the implementation PR t - **Lane 3 Stage 3a.1** ([lane3-self-hosting-cycle.md](./lane3-self-hosting-cycle.md)) — R2 is that sub-stage's design - **DB-1 Correction shape** ([design-correction-shape.md](./design-correction-shape.md)) — cluster termination diagnostics emit Corrections - **DB-7 Symbolic cost** ([design-symbolic-cost-algebra.md](./design-symbolic-cost-algebra.md)) — reads `LoopBound::Descent.cluster` for recursion depth bound -- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field; substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ArityIndex`, `TransformRef`) declared here and consumed by the records above — all added together in the DB-9 Lane 3 Stage 3a.1 implementation PR +- **`src/v3/std/substrate.dag`** — `LoopBound` grows `Descent` variant; `Cluster`, `MemberDescent`, `IntraClusterCall` terminal types added; `type Dag` gains `clusters: List` field; substrate integrity primitives (`NonEmptyList`, `NonSingletonList`, `ParamRef`, `TransformRef`) declared here and consumed by the records above — all added together in the DB-9 Lane 3 Stage 3a.1 implementation PR - **ROADMAP Track 9** — substrate integrity primitives graduation ledger; `IndexedElement.index` in `src/v3/std/list.dag` is the planned second consumer - **`src/v3/compiler/src/dag.rs`** — `Dag.clusters: Vec` sidecar - **`src/v3/compiler/src/lower.rs`** — `compute_mutually_recursive` return upgraded; cluster-Loop construction replaces rejection @@ -395,7 +399,8 @@ R2 landed after a four-round design review. Each round narrowed the shape: ## Changelog -- **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `MemberDescent.position: Int` → `ArityIndex`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives are proposed here as substrate additions; their declarations (`type NonEmptyList`, `type NonSingletonList`, `type ArityIndex`, `type TransformRef`) land in `src/v3/std/substrate.dag` with the DB-9 Lane 3 Stage 3a.1 implementation PR alongside the `Cluster` / `MemberDescent` / `IntraClusterCall` consumers. Track 9 ROADMAP entry captures the ledger and the planned second consumer (`IndexedElement.index`). +- **2026-04-17 R2.1 (ChatGPT-review follow-up)** — on PR #516 sha `1ef38dbd` ChatGPT flagged that pairing `MemberDescent.position: ArityIndex` with `member: NodeId` made only non-negativity structural; the member-relative bound still sat outside the shape, so "out-of-arity is unrepresentable by the type shape" overclaimed the guarantee. Collapsed `MemberDescent { member: NodeId, position: ArityIndex }` → `MemberDescent { param: ParamRef }`, a single typed handle whose sole constructor `param_of(member, slot) -> ParamRef?` fails closed on any invalid (member, slot). "Valid parameter of this member" now lives on the handle, not on constructor prose. `ArityIndex` drops out as a standalone Track 9 primitive. `IndexedElement.index` planned consumer updated to the analogous `ElementRef` pattern. +- **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives are proposed here as substrate additions; their declarations (`type NonEmptyList`, `type NonSingletonList`, `type ParamRef`, `type TransformRef`) land in `src/v3/std/substrate.dag` with the DB-9 Lane 3 Stage 3a.1 implementation PR alongside the `Cluster` / `MemberDescent` / `IntraClusterCall` consumers. Track 9 ROADMAP entry captures the ledger and the planned second consumer (`IndexedElement.index`). - **2026-04-17 R2 post-review** — addressed PR #511 ChatGPT + codex review. Three blocking fixes: (1) reflected `type Dag` gains `clusters: List` so `.dag` lens consumers see the sidecar (facts-flow-forward at lower → lens boundary); (2) `CallEdge { caller, callee }` replaced with `IntraClusterCall { transform: NodeId }` — typed handle into the authoritative `Transform` node, preserves per-call-site identity, removes the second edge authority; (3) `LoopBound` four-pattern dissolution receipt stamped in-doc, not deferred. Non-blocking forbidden-string ratchet extension deferred to Lane 1 Stage 1a per codex suggestion. - **2026-04-17** — R2 landed. Supersedes R1. Director-approved Revised Encoding C (LoopBound coproduct + Dag.clusters sidecar + per-member descent positions). - **2026-04-17** — R1 rejected during review. Lens-level SCC conflicted with INVARIANTS:555 / :665 and introduced parallel representation with `compute_mutually_recursive`. From 1469b22bd9467fed0a5d14eeae2d60fa54e39aad Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 17 Apr 2026 19:18:07 -0400 Subject: [PATCH 4/4] =?UTF-8?q?docs:=20termination-lens=20dual-slot=20walk?= =?UTF-8?q?=20=E2=80=94=20resolve=20caller's=20and=20callee's=20ParamRef?= =?UTF-8?q?=20at=20each=20edge?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ChatGPT REQUEST_CHANGES on PR #516 sha 3910d440e correctly caught that the termination-lens paragraph still described the descent check with a single-slot formulation ("argument at caller's descent slot vs caller's param at same slot"). That silently collapses mixed-position SCCs (e.g. process/help where a's descent is slot 1 and b's is slot 0) back to single-position validation — the new per-member ParamRef carrier would do no work, and the lens would mis-check the wrong argument on heterogeneous SCCs. Fix: rewrite the termination-lens paragraph to walk BOTH members' ParamRef handles at each IntraClusterCall edge: caller_slot = caller's MemberDescent.param.slot_of() callee_slot = callee's MemberDescent.param.slot_of() check: argument at the Transform's callee_slot position is structurally smaller than the caller's formal parameter at caller_slot The check crosses the caller/callee boundary that ParamRef was introduced to preserve — callee_slot selects WHICH ARGUMENT is being fed into the callee's descent param, caller_slot selects WHICH FORMAL is the caller's decreasing measure. Also updated: - Error reporting example now shows both slot labels in the diagnostic body (useful in mixed-position SCCs where they differ) - Acceptance criteria: negative-fixture diagnostic must name BOTH ParamRef handles; added a mixed-position positive-fixture acceptance to regression-guard the callee-side slot usage - Changelog entry for this second ChatGPT-review follow-up Verdict on original review: ChatGPT's principles 1, 2, 4, 5 satisfied already. Principles 3 + 6 (the single BLOCKING class) flip green with this commit — the API's dual handles are now consumed with the generality the doc claims. Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/design-mutual-recursion-lowering.md | 28 +++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/docs/design-mutual-recursion-lowering.md b/docs/design-mutual-recursion-lowering.md index a4420fe8adb..9f031fcb55a 100644 --- a/docs/design-mutual-recursion-lowering.md +++ b/docs/design-mutual-recursion-lowering.md @@ -240,7 +240,20 @@ A cluster called from N external sites produces N `Behavior::Loop` nodes, each r ### Consumers -**Termination lens** (Lane 2 — `src/v3/lenses/termination.dag`, to be created): walks `Behavior::Loop`. When `bound = Descent { cluster }`, reads `Dag.clusters[cluster]` for members. For each `MemberDescent.param: ParamRef`, the lens queries `ParamRef.member_of()` and `ParamRef.slot_of()` to recover the member node and the descent slot. For each `IntraClusterCall.transform: TransformRef` in `intra_cluster_calls`, the lens reaches into the authoritative `Transform` node to read the argument list and verifies the argument at the caller-member's descent slot is structurally smaller than the caller's parameter at the same slot. No SCC re-detection. Diagnostic on failure names the exact Transform (so `transform.span` points at the failing call site — two `a → b` sites diagnose distinctly). +**Termination lens** (Lane 2 — `src/v3/lenses/termination.dag`, to be created): walks `Behavior::Loop`. When `bound = Descent { cluster }`, reads `Dag.clusters[cluster]` for members and builds a map `member_node → ParamRef` by querying each `MemberDescent.param`'s `member_of()` / `slot_of()` accessors. + +For each `IntraClusterCall.transform: TransformRef` in `intra_cluster_calls`, the lens resolves the edge's **caller** (the enclosing Bind of the Transform — looked up via `TransformRef` and an enclosing-Bind walk) and its **callee** (the Bind identified by `transform.target = Callable(decl)` that resolves back to one of the cluster members). It looks up **both** members' `ParamRef` entries: + +- `caller_slot` = the caller member's descent slot (from the caller's `MemberDescent.param.slot_of()`) +- `callee_slot` = the callee member's descent slot (from the callee's `MemberDescent.param.slot_of()`) + +These need not be the same slot — the `process` / `help` case (§"Per-member descent positions") has them at different positions. The check is: + +> The argument at position `callee_slot` in the Transform's argument list (i.e. the value the callsite binds to the callee's descent param) is structurally smaller than the caller's formal parameter at position `caller_slot` (i.e. the caller's descent param). + +This crosses the boundary the `ParamRef` carrier was introduced to preserve: the callee-side slot selects *which argument* is being fed into the callee's decreasing parameter, the caller-side slot selects *which formal* is the caller's decreasing measure, and the structural-smaller check relates the two. A single-slot formulation (comparing "argument at caller's slot" against "caller's param at caller's slot") would silently collapse mixed-position SCCs back into the single-position regime. + +No SCC re-detection. Diagnostic on failure names the exact `TransformRef` (so `transform.span` points at the failing call site — two `a → b` sites diagnose distinctly) plus both `ParamRef` handles so the user can see which caller-param and which callee-param the check was keyed on. **Complexity lens** (Lane 2 — `src/v3/lenses/complexity.dag`): reads `Loop.bound × cost(body)` per the standard cost rule. When `bound = Descent`, the bound reads from the cluster's shared measure. No SCC re-detection. Matches SELF_HOSTING:708-713 verbatim. @@ -289,12 +302,15 @@ ERROR at : mutually-recursive cluster does not terminate fn b(n: Int) -> Int = if n == 0 then 1 else a(n - 1) Cluster: {a, b} -Descent failure: call edge `a → b` passes position 0 without decreasing it. +Descent failure at call `a → b`: + - `a`'s descent param: `n` (slot 0) + - `b`'s descent param: `n` (slot 0) + - Argument at `b`'s slot 0 (`n`) is not structurally smaller than `a`'s slot 0 (`n`). -FIX: decrease position 0 on every intra-cluster call, e.g., `b(n - 1)`. +FIX: on this call, pass a structurally-smaller value at `b`'s descent slot, e.g., `b(n - 1)`. ``` -Uses the DB-1 Correction shape (source-level). The diagnostic names the failing `IntraClusterCall.transform: TransformRef` (typed handle into the authoritative `Transform`, which carries its own `span`) and the `MemberDescent.param: ParamRef` whose slot did not decrease across that intra-cluster edge. "Position 0" in the diagnostic body comes from `ParamRef.slot_of()` on the caller's descent param. +Uses the DB-1 Correction shape (source-level). The diagnostic names the failing `IntraClusterCall.transform: TransformRef` (typed handle into the authoritative `Transform`, which carries its own `span`) plus both `ParamRef` handles — the caller's descent param (for the expected-smaller side) and the callee's descent param (for the slot the argument is being fed into). In the mixed-position case, slot labels in the diagnostic come from the respective `ParamRef.slot_of()` calls and may differ; both are shown so the user can see exactly which caller-formal and which callee-formal the check was keyed on. --- @@ -348,7 +364,8 @@ None blocking. Two deliberately-deferred refinements for the implementation PR t - [ ] Rust / Go / Python emission produces N separate `fn` declarations calling each other **Negative fixtures:** -- [ ] SCC with no shared descent measure (argument preserved or grows on some edge) → fail-closed diagnostic naming the failing `IntraClusterCall.transform: TransformRef`'s span + the caller's `MemberDescent.param: ParamRef` (slot recoverable via `ParamRef.slot_of`) +- [ ] SCC with no shared descent measure (argument preserved or grows on some edge) → fail-closed diagnostic naming the failing `IntraClusterCall.transform: TransformRef`'s span + **both** the caller's and callee's `MemberDescent.param: ParamRef` handles (slots recoverable via `ParamRef.slot_of`; the two slots may differ in mixed-position SCCs) +- [ ] Mixed-position SCC fixture (e.g. `process(state, remaining)` / `help(tasks, state)`) with a valid descent: lens verifies the argument at the *callee*'s descent slot is smaller than the *caller*'s descent param — not the caller's slot — and compiles without diagnostics - [ ] Two distinct `a → b` call sites with different argument shapes produce two distinct `IntraClusterCall` entries; diagnostic differentiates which site failed - [ ] Non-SCC call pattern → single-recursion path unchanged (regression guard) @@ -399,6 +416,7 @@ R2 landed after a four-round design review. Each round narrowed the shape: ## Changelog +- **2026-04-17 R2.1 (ChatGPT-review follow-up #2)** — on PR #516 sha `3910d440e` ChatGPT flagged that the termination-lens prose still validated only caller-aligned positions ("argument at the caller-member's descent slot [vs] the caller's parameter at the same slot"), dropping the callee-side slot that the newly-introduced per-member `ParamRef` carrier was meant to preserve. Under that wording, mixed-position SCCs (e.g. `process` at slot 1, `help` at slot 0) would silently collapse back to single-position validation and mis-check the wrong argument. Termination-lens paragraph rewritten to explicitly resolve **both** members' `ParamRef` handles at each intra-cluster edge: `caller_slot` for the caller's decreasing-formal side, `callee_slot` for the argument-feeding-the-callee side, and the structural-smaller check relates the two across the boundary. Error-reporting example updated to show both slot labels in the diagnostic body. Acceptance criteria tightened: added a mixed-position positive-fixture acceptance, and the negative-fixture diagnostic now must name both `ParamRef` handles rather than just the caller's. - **2026-04-17 R2.1 (ChatGPT-review follow-up)** — on PR #516 sha `1ef38dbd` ChatGPT flagged that pairing `MemberDescent.position: ArityIndex` with `member: NodeId` made only non-negativity structural; the member-relative bound still sat outside the shape, so "out-of-arity is unrepresentable by the type shape" overclaimed the guarantee. Collapsed `MemberDescent { member: NodeId, position: ArityIndex }` → `MemberDescent { param: ParamRef }`, a single typed handle whose sole constructor `param_of(member, slot) -> ParamRef?` fails closed on any invalid (member, slot). "Valid parameter of this member" now lives on the handle, not on constructor prose. `ArityIndex` drops out as a standalone Track 9 primitive. `IndexedElement.index` planned consumer updated to the analogous `ElementRef` pattern. - **2026-04-17 R2.1** — graduated substrate records onto Track 9 substrate integrity primitives. `Cluster.members: List` → `NonSingletonList`; `Cluster.intra_cluster_calls: List` → `NonEmptyList`; `IntraClusterCall.transform: NodeId` → `TransformRef`. Closes the four blockers on PR #511 post-review (chatgpt-auto-review REQUEST_CHANGES, codex-review BLOCKING, three inline BLOCKING comments) by replacing "enforced by construction" with type-shape enforcement. Dissolution-receipt paragraph rewritten to reflect the type-level answer. Primitives are proposed here as substrate additions; their declarations (`type NonEmptyList`, `type NonSingletonList`, `type ParamRef`, `type TransformRef`) land in `src/v3/std/substrate.dag` with the DB-9 Lane 3 Stage 3a.1 implementation PR alongside the `Cluster` / `MemberDescent` / `IntraClusterCall` consumers. Track 9 ROADMAP entry captures the ledger and the planned second consumer (`IndexedElement.index`). - **2026-04-17 R2 post-review** — addressed PR #511 ChatGPT + codex review. Three blocking fixes: (1) reflected `type Dag` gains `clusters: List` so `.dag` lens consumers see the sidecar (facts-flow-forward at lower → lens boundary); (2) `CallEdge { caller, callee }` replaced with `IntraClusterCall { transform: NodeId }` — typed handle into the authoritative `Transform` node, preserves per-call-site identity, removes the second edge authority; (3) `LoopBound` four-pattern dissolution receipt stamped in-doc, not deferred. Non-blocking forbidden-string ratchet extension deferred to Lane 1 Stage 1a per codex suggestion.