From 3ca8704c6b3f7ce1d8c7995782a5d43ce4a3e271 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 18 May 2026 23:03:19 -0400 Subject: [PATCH 1/3] CP-1b/T-8 close bucket A scaffolds --- docs/audit/dissolution-inventory.md | 24 ++++----- src/v4/DECISIONS.md | 6 ++- src/v4/compiler/03_normalize.dag | 61 ++++++++++++----------- src/v4/compiler/03_resolve.dag | 75 +++++++++++++++++++---------- 4 files changed, 96 insertions(+), 70 deletions(-) diff --git a/docs/audit/dissolution-inventory.md b/docs/audit/dissolution-inventory.md index d86c003fb14..4f53fe5ce7a 100644 --- a/docs/audit/dissolution-inventory.md +++ b/docs/audit/dissolution-inventory.md @@ -139,7 +139,7 @@ the audit anchors. | **P2** | `std/collection.dag` Wave-A2: `List where non_empty` refinement **plus** the List combinator algebra (`forall` / `count_where` / `unique` over `FreeMonoid`) | std / T-3 Wave-A2 (coercion-design.md RQ-3) | **5 named + 29 sites** | Section 2: `std/node.dag` × 4 traverses (`all_edges_named`, `all_edges_positional`, `name_occurrences`, `all_names_distinct`). DECISIONS.md: `SL-3229-VERILOG-NONEMPTY` (one row, 29 verilog.dag back-pointer sites after P8). | | **P3** | Compiler pipeline-stage substrate (lex-walk + parse-walk) | compiler / T-6, T-7 | **2 + ~7 in-file** | Section 2: `compiler/01_tokenize.dag tokenize`, `compiler/02_parse.dag parse`. In-file: the parser-side VAGUE prose blocks in `json.dag` / `yaml.dag` / `toml.dag` that concretize to T-6/T-7 (the operations-side family separate from P1). | | **P4** | T-4 fact-bundle Phase-3 rework (post-D2-reversal model) | extdeps/languages / T-4 manager `vivid-carp-207` (5-feeder gate; keystone #3226 merged @`77b9e7d72`; 4 feeders open: T-3, T-29, T-30, T-25-core) | **4 + 1 row + 1 fn** | In-file: `typescript.dag` × 4 INVALID-GATE blocks (re-gate against this arrival, not pre-reversal D2). DECISIONS.md: `SL-3229-VERILOG-D3200` (if re-gated as `feature: T-4 fact-bundle Phase-3 rework` rather than `consumer:` form — see Section 3). Section 2: `extdeps/languages/dag.dag dag_language_model_wave1_void_canonical_symbols` (added in CP-1b #3225 — canonical_symbols set is a fact on DagLanguageModel/language-identity, not a hand-rolled function). | -| **P5** | `std/node.dag` `fold_node` — Node catamorphism (substrate-extension under T-1) | std / T-1 | **1 + 3 (03_resolve cascade only)** | **Substrate LANDED PR #3297:** `NodeFold` + `fold_node` in `src/v4/std/node.dag`; `node_well_formed` consumes the shared `NodeFold` algebra (burn-down closeout + #3297). **Cascade (open):** `compiler/03_resolve.dag merge_binding_self` (94, codex #3225) plus `add_module_named_exports` (99), `add_arrow_domain_named_params` (113), `add_bind_atom_binder` (140). These dissolve to `fold_node(root, ⟨binding-harvest algebra⟩)` only when a scoped harvest algebra lands without changing resolver scope semantics. | +| **P5** | `std/node.dag` `fold_node` — Node catamorphism (substrate-extension under T-1) | std / T-1 | **LANDED for 03_resolve cascade (2026-05-19)** | **Substrate LANDED PR #3297:** `NodeFold` + `fold_node` in `src/v4/std/node.dag`; `node_well_formed` consumes the shared `NodeFold` algebra (burn-down closeout + #3297). **Cascade dissolved:** `compiler/03_resolve.dag` deleted `merge_binding_self`; `add_module_named_exports`, `add_arrow_domain_named_params`, and `add_bind_atom_binder` now consume scoped `NodeFold>` binding-harvest algebras without changing resolver scope semantics. | | **P6** | `std/algebra.dag` / `std/nat.dag` `fold` / `cata` over `FreeMonoid` and `Nat` (Wave-A2) | std / T-3 Wave-A2 | **2** | Section 2: `std/algebra.dag free_monoid_length`, `std/float.dag nat_compare`. (Sibling to P2's combinator algebra; could land in the same PR — kept separate because the underlying primitive is the catamorphism, distinct from `forall`/`count_where` which are derived from it.) | | **P7** | `std/nat.dag nat_is_zero : Nat -> Bool` (Wave-A2) | std / T-3 Wave-A2 | **1** | Section 2: `std/float.dag float_finite_magnitude_zero`. | | **P8** | `extdeps/languages/verilog.dag` bundled T-4 LanguageModel `constant_expression` sub-grammar | extdeps/languages / T-4 Verilog Phase-3 | **0** | Landed: `VectorRange` carries `ConstantExpression` endpoints; DECISIONS.md row `SL-3229-VERILOG-VECTOR-RANGE` is closed. | @@ -331,19 +331,15 @@ follow-up.** The two functions surfaced as #3225's un-cleared codex REQUEST_CHANGES findings (threads `3255338394` / `3255338395`) are captured here as the audit anchor for the rest: -- `merge_binding_self` (94) — 🟡 **walker** (the "sym↦sym module harvest" - codex finding). The leaf helper is `map_insert(m, sym, sym)`, but it - is the symbolic-merge primitive used inside three named-harvest - walkers (`add_module_named_exports` at 99, `add_arrow_domain_named_params` - at 113, `add_bind_atom_binder` at 140) — all three are `fold` over - `Node.children` doing constructor-discriminated recursion. - **Substrate dependency satisfied (PR #3297):** `fold_node` exists in - `std/node.dag`. These four sites are the **P5 cascade** — they still - need a scoped binding-harvest `NodeFold>` (or - equivalent) that preserves resolver scope semantics; not a repeat - T-1 substrate-extension PR. Dissolves to `fold_node(root, ⟨algebra⟩)` - over that algebra; eliminates the three harvest walkers plus the - implicit recursion in `merge_binding_self`'s callers. +- `merge_binding_self` (94) — 🟢 **DISSOLVED 2026-05-19.** The "sym↦sym" + leaf helper is gone. The three binding-harvest sites + (`add_module_named_exports`, `add_arrow_domain_named_params`, + `add_bind_atom_binder`) now consume scoped `NodeFold>` + algebras (`direct_named_edge_binding_fold`, `direct_atom_binding_fold`) + through `fold_node`. The algebras ignore child fold results where the + resolver contract requires direct children only, preserving module, + arrow-domain, and arity-3 `Bind` scope semantics while deleting the + local `Node.children` folds. - The other 22 fns in 03_resolve.dag (`empty_namespace`, `empty_canonical_symbol_set`, `build_program_namespace`, diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index 3f3595f7496..cf47b95b3c1 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -196,9 +196,9 @@ consumes that derived fact. 4. **`SurfaceSugarKind` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold):** T-8 normalize seam; not a terminal substrate primitive while the stage is scaffold. **Dissolution pattern — enumerated axis (closed N=4):** names the four C3 surface-sugar connectives aligned with the `data dag_c3_surface_sugar_*` identities in `extdeps/languages/dag.dag` (THESIS/C3; not a foreign-label consumer coproduct). **Named triggers:** `classify_sugar`; feeds `normalize_node` / `malformed_sugar_diagnostic`. -5. **`SugarClassification` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — partition:** `Sugar` vs `NotSugar` splits the normalize walk between C3-shaped sugar and pass-through `Node` kinds. **Named triggers:** `classify_sugar`; `normalize_node`; `normalize_edge`. +5. **`SugarClassification` (`compiler/03_normalize.dag`):** **DISSOLVED 2026-05-19.** The local `Sugar | NotSugar` carrier was replaced by the existing optional carrier: `classify_sugar(n) -> SurfaceSugarKind?`. The remaining `SurfaceSugarKind` axis is item 4; absence is now the canonical `None` branch, not a second stage-local coproduct. -6. **`NormalizeChildrenResult` (`compiler/03_normalize.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — success-or-Diagnostic carrier:** `NormalizedChildren` vs `NormalizeChildrenRejected` threads child recursion fail-closed without a second authority. **Named triggers:** `normalize_children`; `normalize_edge` / `normalize_node` folds. +6. **`NormalizeChildrenResult` (`compiler/03_normalize.dag`):** **DISSOLVED 2026-05-19.** The local success-or-diagnostic carrier was replaced by the canonical `Outcome>` from `std/diagnostic.dag`; `normalize_children`, `normalize_edge`, and `normalize_node` now share the same fail-closed carrier. 7. **`Scope` (`compiler/03_resolve.dag`):** **Classification — 🟡 YELLOW (scaffold).** **Dissolution pattern — structured lexical environment:** `ScopeRoot` (module `Namespace`) vs `ScopeFrame` (locals + outer) for K-1 use→def binding (B-4; Part 1 **B-4** row). **Named triggers:** `resolve_node`; `resolve_atom`; `resolve_bind_*` family. @@ -212,6 +212,8 @@ consumes that derived fact. 12. **`std/node.dag` — `is_empty_conj_root` (P5 / INVARIANTS §Progress Is Dissolution; codex PR #3284):** **Not a net-new `is_*` verifier** — this is the **landed R1 receipt** from `docs/audit/dissolution-inventory.md` §1.0: one structural query replaces three literal duplicate predicates (`compiler/01_tokenize.dag`, `compiler/02_parse.dag`, `extdeps/languages/dag.dag`). **Interim steady-state:** shared empty-`Conj`-root shape leg for wave-1 void LM / E0–G0 stubs until T-6/T-7 generic walks consume grammar-as-data without re-deriving this `match`. **Forward dissolution (named triggers):** (a) `fold_node` / `NodeFold` in `std/node.dag` is **landed** (dissolution-inventory **P5** substrate — PR #3297; `node_well_formed` is already a consumer). Optional follow-up: fold this discriminant into that catamorphism / shared query surface if a ratified consumer wants to shed the dedicated `match`. Remaining **P5** debt is the **`compiler/03_resolve.dag` binding-harvest cascade** (inventory §2.3), not absent substrate. (b) `feature: compiler pipeline-stage lex-walk + parse-walk substrate` (inventory **P3**, TASKS T-6/T-7) — grammar-as-data carries void-book as constructor-shaped facts so consumers discriminate on `NodeKind` / carriers instead of calling `is_empty_conj_root`. **Audit anchor:** inventory §1.0 row **R1** (status = landed PR #3284). **Api-review receipt (PR #3274):** duplicate-collapse / modeling-discipline Practice 5 single authority — not a parallel verification predicate. **INVARIANTS.md §P5 — Dispatch-Discipline Mechanisms (b)** SG-0 `EXPECTED_HAND_AUTHORED_*` census gates **new** `src/v3/compiler/tests/**` hand-Rust paths; they do **not** apply to this v4-only substrate `fn`. **Exhaustiveness:** `NodeKind` is the closed `TypeNode | ComputationNode` pair today; a third top-level variant would require updating every `match n.kind` in `std/node.dag`, including this helper, in the same substrate edit that extends `NodeKind`. +12a. **`compiler/03_resolve.dag` — binding-harvest cascade (P5):** **DISSOLVED 2026-05-19.** The local `merge_binding_self` leaf plus three direct child walkers (`add_module_named_exports`, `add_arrow_domain_named_params`, `add_bind_atom_binder`) now route through scoped `NodeFold>` algebras: `direct_named_edge_binding_fold` for direct `Conj` named-edge harvest and `direct_atom_binding_fold` for the arity-3 `Bind` binder slot. The algebras intentionally ignore child fold results where resolver scope semantics require direct children only; the recursion surface is the canonical `fold_node` substrate primitive, not hand recursion over `Node.children`. + 13a. **`LexCharClass` (`compiler/01_tokenize.dag`):** **Classification — 🟡 YELLOW (P3-gated declarative seam).** **Dissolution pattern — closed character-class vocabulary:** variants name the lexical character classes the future T-6 walk consumes. **Named triggers:** `feature:T-6`; consumed by `LexPattern.CharClassPattern`. 13b. **`LexPattern` (`compiler/01_tokenize.dag`):** **Classification — 🟡 YELLOW (P3-gated declarative seam).** **Dissolution pattern — regular-language grammar carrier:** atoms plus sequence/choice/optional/repeat declare lexical productions as data; the current tokenizer does not walk them. **Named triggers:** `feature:T-6`; `consumer:compiler/01_tokenize.tokenize`; future P3 lexical walk consumes this carrier directly. diff --git a/src/v4/compiler/03_normalize.dag b/src/v4/compiler/03_normalize.dag index f63a90da54c..932830a702e 100644 --- a/src/v4/compiler/03_normalize.dag +++ b/src/v4/compiler/03_normalize.dag @@ -1,7 +1,7 @@ // src/v4/compiler/03_normalize.dag // // Scope: Stage 3a — ParseTree→NormalizedTree; C3 sugar to Node. -// Owns: NormalizedTree; SurfaceSugarKind; SugarClassification; normalize; stage Symbol reasons. +// Owns: NormalizedTree; SurfaceSugarKind; normalize; stage Symbol reasons. // Consumes: std/node.dag, std/diagnostic.dag, compiler/02_parse.dag, extdeps/languages/dag.dag. // Status: scaffold — TASKS T-8. // Anchor: https://en.wikipedia.org/wiki/Abstract_syntax_tree @@ -48,34 +48,38 @@ type SurfaceSugarKind | OperationSugar -// 🟡 coproduct dissolution — DECISIONS.md CP-1b item 5 (SugarClassification) -type SugarClassification - = Sugar { kind: SurfaceSugarKind } - | NotSugar +fn some_surface_sugar_kind(kind: SurfaceSugarKind) -> SurfaceSugarKind? { + Some { value: kind } +} + + +fn no_surface_sugar_kind() -> SurfaceSugarKind? { + None +} -fn classify_sugar(n: Node) -> SugarClassification { +fn classify_sugar(n: Node) -> SurfaceSugarKind? { match n.kind { TypeNode { connective: Atom { identity: id } } => if id == dag_c3_surface_sugar_service { - Sugar { kind: ServiceSugar } + some_surface_sugar_kind(kind: ServiceSugar) } else { if id == dag_c3_surface_sugar_fn { - Sugar { kind: FnSugar } + some_surface_sugar_kind(kind: FnSugar) } else { if id == dag_c3_surface_sugar_type { - Sugar { kind: TypeSugar } + some_surface_sugar_kind(kind: TypeSugar) } else { if id == dag_c3_surface_sugar_operation { - Sugar { kind: OperationSugar } + some_surface_sugar_kind(kind: OperationSugar) } else { - NotSugar + no_surface_sugar_kind() } } } } - TypeNode { connective: _ } => NotSugar - ComputationNode { behavior: _ } => NotSugar + TypeNode { connective: _ } => no_surface_sugar_kind() + ComputationNode { behavior: _ } => no_surface_sugar_kind() } } @@ -117,25 +121,24 @@ fn normalize_edge(e: Edge) -> Outcome { } -// 🟡 coproduct dissolution — DECISIONS.md CP-1b item 6 (NormalizeChildrenResult) -type NormalizeChildrenResult - = NormalizedChildren { children: List } - | NormalizeChildrenRejected { diagnostic: Diagnostic } +fn empty_normalized_children() -> Outcome> { + Produced { value: Empty } +} -fn normalize_children(children: List) -> NormalizeChildrenResult { - fold(children, init: NormalizedChildren { children: [] }, f: fn(acc, e) { +fn normalize_children(children: List) -> Outcome> { + fold(children, init: empty_normalized_children(), f: fn(acc, e) { match acc { - NormalizeChildrenRejected { diagnostic: d } => - NormalizeChildrenRejected { diagnostic: d } - NormalizedChildren { children: done } => + Rejected { diagnostic: d } => + Rejected { diagnostic: d } + Produced { value: done } => match normalize_edge(e: e) { Produced { value: normalized_edge } => - NormalizedChildren { - children: list_push(done, normalized_edge) + Produced { + value: list_push(done, normalized_edge) } Rejected { diagnostic: d } => - NormalizeChildrenRejected { diagnostic: d } + Rejected { diagnostic: d } } } }) @@ -205,12 +208,12 @@ fn normalize_sugar(kind: SurfaceSugarKind, n: Node, children: List) -> Out fn normalize_node(n: Node) -> Outcome { match normalize_children(children: n.children) { - NormalizeChildrenRejected { diagnostic: d } => Rejected { diagnostic: d } - NormalizedChildren { children: normalized_children } => + Rejected { diagnostic: d } => Rejected { diagnostic: d } + Produced { value: normalized_children } => match classify_sugar(n: n) { - Sugar { kind: kind } => + Some { value: kind } => normalize_sugar(kind: kind, n: n, children: normalized_children) - NotSugar => + None => Produced { value: Node { kind: n.kind, diff --git a/src/v4/compiler/03_resolve.dag b/src/v4/compiler/03_resolve.dag index 9671686b3d6..280812e58bc 100644 --- a/src/v4/compiler/03_resolve.dag +++ b/src/v4/compiler/03_resolve.dag @@ -29,8 +29,10 @@ import v4.std.node { Conj, Edge, Node, + NodeFold, Symbol, TypeNode, + fold_node, node_well_formed } @@ -91,42 +93,69 @@ fn empty_canonical_symbol_set() -> Set { } -fn merge_binding_self(m: Map, sym: Symbol) -> Map { - map_insert(m, sym, sym) +fn direct_named_edge_binding_fold(base: Map) -> NodeFold> { + NodeFold { + init: fn(_) { + base + }, + step: fn(acc, e, _) { + match e.label { + Named { name: sym } => map_insert(acc, sym, sym) + Positional => acc + } + } + } } -fn add_module_named_exports(root: Node, acc: Map) -> Map { +fn direct_atom_binding_fold(base: Map) -> NodeFold> { + NodeFold { + init: fn(n0) { + match n0.kind { + TypeNode { connective: Atom { identity: sym } } => + map_insert(base, sym, sym) + _ => base + } + }, + step: fn(acc, _, _) { + acc + } + } +} + + +fn harvest_conj_named_bindings(root: Node, acc: Map) -> Map { match root.kind { TypeNode { connective: Conj } => - fold(root.children, init: acc, f: fn(acc2, e) { - match e.label { - Named { name: decl } => merge_binding_self(m: acc2, sym: decl) - Positional => acc2 - } - }) + fold_node( + n: root, + algebra: direct_named_edge_binding_fold(base: acc) + ) _ => acc } } +fn harvest_direct_atom_binding(root: Node, acc: Map) -> Map { + fold_node( + n: root, + algebra: direct_atom_binding_fold(base: acc) + ) +} + + +fn add_module_named_exports(root: Node, acc: Map) -> Map { + harvest_conj_named_bindings(root: root, acc: acc) +} + + fn add_arrow_domain_named_params(n: Node, acc: Map) -> Map { match n.kind { TypeNode { connective: Arrow } => if count(n.children) >= 1 { match first(n.children) { Some { value: e0 } => - match e0.target.kind { - TypeNode { connective: Conj } => - fold(e0.target.children, init: acc, f: fn(acc2, pe) { - match pe.label { - Named { name: param } => - merge_binding_self(m: acc2, sym: param) - Positional => acc2 - } - }) - _ => acc - } + harvest_conj_named_bindings(root: e0.target, acc: acc) None => acc } } else { @@ -143,11 +172,7 @@ fn add_bind_atom_binder(n: Node, acc: Map) -> Map - match e0.target.kind { - TypeNode { connective: Atom { identity: b } } => - merge_binding_self(m: acc, sym: b) - _ => acc - } + harvest_direct_atom_binding(root: e0.target, acc: acc) None => acc } } else { From e35f28a5a9ab67ec856cac5c67d0799f0d31555f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 03:22:16 +0000 Subject: [PATCH 2/3] Clarify CP-1b P5 cascade closure --- src/v4/DECISIONS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v4/DECISIONS.md b/src/v4/DECISIONS.md index cf47b95b3c1..a9aa0b8d788 100644 --- a/src/v4/DECISIONS.md +++ b/src/v4/DECISIONS.md @@ -210,7 +210,7 @@ consumes that derived fact. 11. **`compiler/01_tokenize.dag` — `LexRules` / wave-1 E0 (T-6 / B2-OMNI; PR #3284 → T-8 spine update #3311):** lexical authority is the typed coproduct `LexRules = VoidLexRules | ModeledLexRules { root: LexRuleSet }`, with rule rows carried by `LexRule` payloads rather than ad-hoc `Node` variant tags. Each `TokenRule.pattern` is a bounded `LexPattern` regular-language carrier (`EmptyPattern`, literal/char/class atoms, sequence, choice, optional, repeat), not a raw `Node` bridge. Wave-1 E0 void lex is `VoidLexRules`. `ModeledLexRules` fail-closes with `tokenize_lexical_walk_not_realized` until the P3 lexical walk primitive lands; no hand-rolled walker is introduced. Rationale lives here per Practice 9; `01_tokenize.dag` carries no in-file rationale beyond the mandated terse header (path + Scope/Owns/Consumes/Status + optional `Anchor:`) and the one-line tags on the tokenize coproducts. -12. **`std/node.dag` — `is_empty_conj_root` (P5 / INVARIANTS §Progress Is Dissolution; codex PR #3284):** **Not a net-new `is_*` verifier** — this is the **landed R1 receipt** from `docs/audit/dissolution-inventory.md` §1.0: one structural query replaces three literal duplicate predicates (`compiler/01_tokenize.dag`, `compiler/02_parse.dag`, `extdeps/languages/dag.dag`). **Interim steady-state:** shared empty-`Conj`-root shape leg for wave-1 void LM / E0–G0 stubs until T-6/T-7 generic walks consume grammar-as-data without re-deriving this `match`. **Forward dissolution (named triggers):** (a) `fold_node` / `NodeFold` in `std/node.dag` is **landed** (dissolution-inventory **P5** substrate — PR #3297; `node_well_formed` is already a consumer). Optional follow-up: fold this discriminant into that catamorphism / shared query surface if a ratified consumer wants to shed the dedicated `match`. Remaining **P5** debt is the **`compiler/03_resolve.dag` binding-harvest cascade** (inventory §2.3), not absent substrate. (b) `feature: compiler pipeline-stage lex-walk + parse-walk substrate` (inventory **P3**, TASKS T-6/T-7) — grammar-as-data carries void-book as constructor-shaped facts so consumers discriminate on `NodeKind` / carriers instead of calling `is_empty_conj_root`. **Audit anchor:** inventory §1.0 row **R1** (status = landed PR #3284). **Api-review receipt (PR #3274):** duplicate-collapse / modeling-discipline Practice 5 single authority — not a parallel verification predicate. **INVARIANTS.md §P5 — Dispatch-Discipline Mechanisms (b)** SG-0 `EXPECTED_HAND_AUTHORED_*` census gates **new** `src/v3/compiler/tests/**` hand-Rust paths; they do **not** apply to this v4-only substrate `fn`. **Exhaustiveness:** `NodeKind` is the closed `TypeNode | ComputationNode` pair today; a third top-level variant would require updating every `match n.kind` in `std/node.dag`, including this helper, in the same substrate edit that extends `NodeKind`. +12. **`std/node.dag` — `is_empty_conj_root` (P5 / INVARIANTS §Progress Is Dissolution; codex PR #3284):** **Not a net-new `is_*` verifier** — this is the **landed R1 receipt** from `docs/audit/dissolution-inventory.md` §1.0: one structural query replaces three literal duplicate predicates (`compiler/01_tokenize.dag`, `compiler/02_parse.dag`, `extdeps/languages/dag.dag`). **Interim steady-state:** shared empty-`Conj`-root shape leg for wave-1 void LM / E0–G0 stubs until T-6/T-7 generic walks consume grammar-as-data without re-deriving this `match`. **Forward dissolution (named triggers):** (a) `fold_node` / `NodeFold` in `std/node.dag` is **landed** (dissolution-inventory **P5** substrate — PR #3297; `node_well_formed` is already a consumer). Optional follow-up: fold this discriminant into that catamorphism / shared query surface if a ratified consumer wants to shed the dedicated `match`; the separate `compiler/03_resolve.dag` binding-harvest cascade that depended on the same substrate is closed in item 12a. (b) `feature: compiler pipeline-stage lex-walk + parse-walk substrate` (inventory **P3**, TASKS T-6/T-7) — grammar-as-data carries void-book as constructor-shaped facts so consumers discriminate on `NodeKind` / carriers instead of calling `is_empty_conj_root`. **Audit anchor:** inventory §1.0 row **R1** (status = landed PR #3284). **Api-review receipt (PR #3274):** duplicate-collapse / modeling-discipline Practice 5 single authority — not a parallel verification predicate. **INVARIANTS.md §P5 — Dispatch-Discipline Mechanisms (b)** SG-0 `EXPECTED_HAND_AUTHORED_*` census gates **new** `src/v3/compiler/tests/**` hand-Rust paths; they do **not** apply to this v4-only substrate `fn`. **Exhaustiveness:** `NodeKind` is the closed `TypeNode | ComputationNode` pair today; a third top-level variant would require updating every `match n.kind` in `std/node.dag`, including this helper, in the same substrate edit that extends `NodeKind`. 12a. **`compiler/03_resolve.dag` — binding-harvest cascade (P5):** **DISSOLVED 2026-05-19.** The local `merge_binding_self` leaf plus three direct child walkers (`add_module_named_exports`, `add_arrow_domain_named_params`, `add_bind_atom_binder`) now route through scoped `NodeFold>` algebras: `direct_named_edge_binding_fold` for direct `Conj` named-edge harvest and `direct_atom_binding_fold` for the arity-3 `Bind` binder slot. The algebras intentionally ignore child fold results where resolver scope semantics require direct children only; the recursion surface is the canonical `fold_node` substrate primitive, not hand recursion over `Node.children`. From 31a46c4f73ac9e7d328503e9d0db13ec20b97d6c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 19 May 2026 04:51:26 +0000 Subject: [PATCH 3/3] Close P5 cascade inventory rollups --- docs/audit/dissolution-inventory.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/audit/dissolution-inventory.md b/docs/audit/dissolution-inventory.md index 4f53fe5ce7a..0d6037327db 100644 --- a/docs/audit/dissolution-inventory.md +++ b/docs/audit/dissolution-inventory.md @@ -169,7 +169,7 @@ INVALID-GATE-once-re-gated): | P2 lands | 5 named (+ 29 verilog sites converge in one sweep) | `std/collection.dag` Wave-A2 | ~11 named | | P3 lands | 2 named (+ ~7 in-file) | T-6 + T-7 pipeline substrate | ~9 named | | P4 lands | 4 + 1 row + 1 fn (`dag.dag canonical_symbols` #3225) | T-4 fact-bundle Phase-3 | ~3 named | -| P5 cascade lands | 1 named (+ 3 walker sites in `03_resolve.dag` #3225) | scoped binding-harvest `fold_node` algebra (substrate: **#3297**) | ~1 | +| P5 cascade landed | 0 | scoped binding-harvest `fold_node` algebra in `03_resolve.dag` (substrate: **#3297**) | no open P5 cascade debt | | P6 lands | 2 | FreeMonoid/Nat catamorphism | ~0 | | P7 lands | 1 | `nat_is_zero` | ~0 | | P9 landed | 0 | `lens/cost.dag` T-12 | ~0 | @@ -740,7 +740,7 @@ fixes are downstream lane work, not C1's** — C1 marks and flags. | class | 🔴 dissolve-now | 🟡 gated (named feature: / consumer:) | 🟢 terminal | |---|---|---|---| -| walker | — | 2 (`std/algebra.dag free_monoid_length` → `fold FreeMonoid`; `std/float.dag nat_compare` → `fold Nat`) + **P5 cascade** (`compiler/03_resolve.dag` binding-harvest sites → scoped `fold_node` algebra; substrate **#3297**) | rest | +| walker | — | 2 (`std/algebra.dag free_monoid_length` → `fold FreeMonoid`; `std/float.dag nat_compare` → `fold Nat`) | rest; **P5 cascade closed** (`compiler/03_resolve.dag` binding-harvest sites consume scoped `fold_node` algebra; substrate **#3297**) | | traverse | — | 4 (`std/node.dag` × 4: → `forall` / `count_where` / `unique` over `FreeMonoid` in `std/collection.dag` Wave-A2) | rest | | predicate | empty-`Conj` R1 predicate **landed** PR #3284 (`std/node.dag` `is_empty_conj_root`, `DECISIONS.md` §CP-1b item 12); LLVM R2 predicate **landed** PR #3245 (`terminator_is_catchswitch` deleted; `block_well_formed` consumes `CatchSwitch` directly) | 3 (`std/node.dag connective_edge_discipline` → per-`Connective` discipline fact; `std/float.dag float_finite_magnitude_zero` → `nat_is_zero`; `extdeps/languages/llvm_ir.dag feature_disposition` → per-feature disposition fact (T-4 fact-bundle)); `llvm_instruction_cost` **landed** under `lens/cost.dag`. | rest | | carrier | — | — | lane-wide | @@ -751,7 +751,7 @@ fixes are downstream lane work, not C1's** — C1 marks and flags. dissolve-on-arrival rule): 1. ~~`fold_node` — `Node` catamorphism in `std/node.dag` (substrate-extension - under T-1).~~ **LANDED PR #3297** (`NodeFold`, `fold_node`; `node_well_formed` is a consumer). **P5 cascade** (binding-harvest in `03_resolve.dag`) remains open under a scoped algebra, not absent substrate. + under T-1).~~ **LANDED PR #3297** (`NodeFold`, `fold_node`; `node_well_formed` is a consumer). **P5 cascade closed 2026-05-19:** binding-harvest in `03_resolve.dag` consumes scoped `NodeFold>` algebras. 2. `fold` / `cata` over `FreeMonoid` and `Nat` in `std/algebra.dag` / `std/nat.dag` (Wave-A2). 3. `forall`, `count_where`, `unique` over `FreeMonoid` in