COMPREP wave-1: Arrow.body substrate + MVP add body producer

src/v4/compiler/03_body_producer.dag

@@ -0,0 +1,176 @@
+// src/v4/compiler/03_body_producer.dag
+// Scope: COMPREP wave-1 — parse-tree / surface expression → Behavior sub-DAG; Arrow.body attachment.
+// Status: keystone producer slice — MVP add(x,y)=x+y body construction + E-9 edge attach.
+// Anchor: docs/design-computation-representation.md wave 1; INVARIANTS E-9.
+
+module v4.compiler.body_producer
+
+import v4.std.algebra { list_snoc_item }
+import v4.std.diagnostic {
+  Accepted,
+  Diagnostic,
+  ExternalContractUnknown,
+  Outcome,
+  Rejected,
+  Unavailable,
+  bind_outcome,
+  node_locus,
+  outcome_accepted,
+  outcome_rejected
+}
+import v4.std.node {
+  Arrow,
+  Atom,
+  ComputationNode,
+  Conj,
+  Edge,
+  Named,
+  Node,
+  Positional,
+  Symbol,
+  Transform,
+  TypeNode,
+  Value,
+  arrow_body_edge,
+  well_formed
+}
+import v4.std.node_query { find_arrow_body_child }
+
+data body_producer_reason_malformed_attachment: Symbol = body_producer_reason_malformed_attachment
+data body_producer_reason_post_produce_not_well_formed: Symbol = body_producer_reason_post_produce_not_well_formed
+
+fn body_producer_diagnostic(reason: Symbol, n: Node) -> Diagnostic {
+  Diagnostic {
+    reason: reason,
+    at: node_locus(node: n),
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn type_atom_node(identity: Symbol) -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: identity } },
+    children: []
+  }
+}
+
+fn computation_param_ref_node(identity: Symbol) -> Node {
+  type_atom_node(identity: identity)
+}
+
+fn attach_arrow_body(arrow: Node, body: Node) -> Outcome<Node> {
+  match arrow.kind {
+    TypeNode { connective: Arrow } =>
+      outcome_accepted(
+        value: Node {
+          kind: arrow.kind,
+          children: list_snoc_item(
+            xs: arrow.children,
+            item: Edge {
+              label: Named { name: arrow_body_edge },
+              target: body
+            }
+          )
+        }
+      )
+    _ =>
+      outcome_rejected(
+        d: body_producer_diagnostic(
+          reason: body_producer_reason_malformed_attachment,
+          n: arrow
+        )
+      )
+  }
+}
+
+// MVP add body: Transform(+) with positional param references (body-scope resolve follows).
+fn produce_mvp1_add_binary_body() -> Node {
+  Node {
+    kind: ComputationNode { behavior: Transform },
+    children: [
+      Edge {
+        label: Positional,
+        target: type_atom_node(identity: ^dag_token_plus)
+      },
+      Edge {
+        label: Positional,
+        target: computation_param_ref_node(identity: ^dag_binding_param_x)
+      },
+      Edge {
+        label: Positional,
+        target: computation_param_ref_node(identity: ^dag_binding_param_y)
+      }
+    ]
+  }
+}
+
+fn produce_mvp1_add_arrow_signature() -> Node {
+  Node {
+    kind: TypeNode { connective: Arrow },
+    children: [
+      Edge {
+        label: Positional,
+        target: type_atom_node(identity: ^dag_binding_type_int)
+      },
+      Edge {
+        label: Positional,
+        target: type_atom_node(identity: ^dag_binding_type_int)
+      },
+      Edge {
+        label: Positional,
+        target: type_atom_node(identity: ^dag_binding_type_int)
+      }
+    ]
+  }
+}
+
+fn produce_mvp1_add_arrow_with_body() -> Outcome<Node> {
+  bind_outcome(
+    o: attach_arrow_body(
+      arrow: produce_mvp1_add_arrow_signature(),
+      body: produce_mvp1_add_binary_body()
+    ),
+    f: fn(arrow_with_body) {
+      if well_formed(n: arrow_with_body) {
+        outcome_accepted(value: arrow_with_body)
+      } else {
+        outcome_rejected(
+          d: body_producer_diagnostic(
+            reason: body_producer_reason_post_produce_not_well_formed,
+            n: arrow_with_body
+          )
+        )
+      }
+    }
+  )
+}
+
+fn produce_mvp1_add_decl_node(fn_name: Symbol) -> Outcome<Node> {
+  bind_outcome(
+    o: produce_mvp1_add_arrow_with_body(),
+    f: fn(arrow_with_body) {
+      outcome_accepted(
+        value: Node {
+          kind: TypeNode { connective: Conj },
+          children: [
+            Edge {
+              label: Named { name: fn_name },
+              target: arrow_with_body
+            }
+          ]
+        }
+      )
+    }
+  )
+}
+
+fn arrow_has_body_edge(arrow: Node) -> Bool {
+  match find_arrow_body_child(root: arrow) {
+    Accepted { value: body, diagnostics: _ } =>
+      match body.kind {
+        ComputationNode { behavior: _ } => true
+        _ => false
+      }
+    Rejected { diagnostics: _ } => false
+  }
+}

src/v4/std/node.dag

@@ -83,6 +83,8 @@ type Edge {
 }
 // 🟡 gated — substrate-shape bridge (docs/modeling-discipline.md Practice 2/10) — feature: node-behavior-loop-bound-edge-tag — owner: T-12 LoopBound cost-lens wiring — lane: shared Interval<D> parent for Loop measure facts — dissolve-on-arrival: replace Symbol-tagged Loop bound attachment with structural Loop-bound coordinate owned by the interval/bound substrate; forbidden: new Loop-bound consumers matching raw Named(loop_bound_edge) outside std.node/std.cardinality.
 data loop_bound_edge: Symbol = ^loop_bound_edge
+// 🟢 TERMINAL — E-9/DB-14: Arrow.body is the single authority for internal (Behavior sub-DAG) and external realization.
+data arrow_body_edge: Symbol = ^arrow_body_edge
 type Node {
   kind: NodeKind
   children: List<Edge>
@@ -103,12 +105,14 @@ type EdgeDiscipline
   | PositionalEdges
   // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-edge-discipline — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: Loop edge discipline as EdgeDiscipline arm consumed by edges_conform and content_hash canonicalization; forbidden: parallel PositionalEdges classifier for Loop outside loop_behavior_edges_conform.
   | LoopBoundEdges
+  // 🟢 TERMINAL — COMPREP wave 0/1: Arrow signature positional edges + optional Arrow.body named edge (design-computation-representation.md; INVARIANTS E-9).
+  | ArrowBodyEdges
 fn connective_edge_discipline(c: Connective) -> EdgeDiscipline {
   match c {
     Atom { identity: _ } => NoEdges
     Conj => LabeledEdges
     Disj => LabeledEdges
-    Arrow => PositionalEdges
+    Arrow => ArrowBodyEdges
     Cardinality => PositionalEdges
     Instantiation => PositionalEdges
   }
@@ -147,15 +151,18 @@ fn name_occurrences(name: Symbol, children: List<Edge>) -> Int {
     }
   })
 }
-// 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-positional-count — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: substrate Loop positional-child count query; forbidden: parallel ad-hoc Loop arity predicates outside well_formed.
-fn loop_positional_child_count(children: List<Edge>) -> Int {
+fn positional_child_count(children: List<Edge>) -> Int {
   fold(children, init: 0, f: fn(acc, e) {
     match e.label {
       Positional => acc + 1
       Named { name: _ } => acc
     }
   })
 }
+// 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-positional-count — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: substrate Loop positional-child count query; forbidden: parallel ad-hoc Loop arity predicates outside well_formed.
+fn loop_positional_child_count(children: List<Edge>) -> Int {
+  positional_child_count(children: children)
+}
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-edge-discipline — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: substrate Loop edge-discipline query shared by well_formed and cardinality witnesses; forbidden: parallel ad-hoc Loop edge predicates outside well_formed.
 fn loop_body_edges_conform(children: List<Edge>) -> Bool {
   fold(children, init: true, f: fn(acc, e) {
@@ -172,6 +179,21 @@ fn loop_behavior_edges_conform(children: List<Edge>) -> Bool {
   && loop_body_edges_conform(children: children)
   && (loop_positional_child_count(children: children) >= 1)
 }
+// 🟢 TERMINAL — COMPREP: Arrow positional signature edges + at most one Arrow.body edge.
+fn arrow_signature_edges_conform(children: List<Edge>) -> Bool {
+  fold(children, init: true, f: fn(acc, e) {
+    match e.label {
+      Positional => acc
+      Named { name: sym } => acc && (sym == ^arrow_body_edge)
+    }
+  })
+}
+fn arrow_body_edges_conform(children: List<Edge>) -> Bool {
+  let body_edges = name_occurrences(name: ^arrow_body_edge, children: children)
+  (body_edges <= 1)
+  && arrow_signature_edges_conform(children: children)
+  && (positional_child_count(children: children) >= 1)
+}
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-bound-measure-target — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: substrate Loop loop_bound_edge target projection shared by cardinality witness; forbidden: parallel ad-hoc loop_bound_edge extraction outside well_formed/cardinality.
 type LoopMeasureTargetLookup
   = Found { target: Node }
@@ -224,6 +246,7 @@ fn edges_conform(children: List<Edge>, d: EdgeDiscipline) -> Bool {
       all_edges_named(children: children) && all_names_distinct(children: children)
     PositionalEdges => all_edges_positional(children: children)
     LoopBoundEdges => loop_behavior_edges_conform(children: children)
+    ArrowBodyEdges => arrow_body_edges_conform(children: children)
   }
 }
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-connective-arity-well-formed — bind node://adhoc-c28e191d-684 — dissolve-on-arrival: substrate Connective arity query over positional child count; forbidden: parallel ad-hoc arity predicates outside well_formed.
@@ -232,8 +255,7 @@ fn connective_edges_conform(children: List<Edge>, c: Connective) -> Bool {
     Atom { identity: _ } => edges_conform(children: children, d: NoEdges)
     Conj => edges_conform(children: children, d: LabeledEdges)
     Disj => edges_conform(children: children, d: LabeledEdges)
-    Arrow =>
-      edges_conform(children: children, d: PositionalEdges) && (count(children) >= 1)
+    Arrow => arrow_body_edges_conform(children: children)
     Cardinality =>
       edges_conform(children: children, d: PositionalEdges) && (count(children) >= 1)
     Instantiation =>
@@ -315,6 +337,33 @@ fn named_edge_sort_key(e: Edge) -> Symbol {
   }
 }
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-behavior-loop-content-hash-canonicalization — bind B1-CANON content_hash — dissolve-on-arrival: Loop/LabeledEdges child reorder scoped to content_hash merkle fold; forbidden: parallel ad-hoc loop_bound_edge placement canonicalization outside this surface.
+fn arrow_signature_edges_for_content_hash(children: List<Edge>) -> List<Edge> {
+  filter(children, e => match e.label { Positional => true, Named { name: _ } => false })
+}
+fn arrow_body_edges_for_content_hash(children: List<Edge>) -> List<Edge> {
+  filter(children, e => match e.label {
+    Named { name: sym } => sym == ^arrow_body_edge
+    Positional => false
+  })
+}
+fn arrow_other_named_edges_for_content_hash(children: List<Edge>) -> List<Edge> {
+  sort_by(
+    filter(children, e => match e.label {
+      Named { name: sym } => sym != ^arrow_body_edge
+      Positional => false
+    }),
+    e => named_edge_sort_key(e: e)
+  )
+}
+fn canonicalize_arrow_children_for_content_hash(children: List<Edge>) -> List<Edge> {
+  concat(
+    arrow_signature_edges_for_content_hash(children: children),
+    concat(
+      arrow_other_named_edges_for_content_hash(children: children),
+      arrow_body_edges_for_content_hash(children: children)
+    )
+  )
+}
 fn loop_body_edges_for_content_hash(children: List<Edge>) -> List<Edge> {
   filter(children, e => match e.label { Positional => true, Named { name: _ } => false })
 }
@@ -351,6 +400,11 @@ fn canonicalize_node_for_content_hash(n: Node) -> Node {
       }
     NoEdges => n
     PositionalEdges => n
+    ArrowBodyEdges =>
+      Node {
+        kind: n.kind,
+        children: canonicalize_arrow_children_for_content_hash(children: n.children)
+      }
     LoopBoundEdges =>
       Node {
         kind: n.kind,

src/v4/std/node_query.dag

@@ -20,7 +20,18 @@ import v4.std.diagnostic {
   outcome_rejected
 }
 import v4.std.algebra { Empty, list_snoc_item }
-import v4.std.node { Conj, Edge, Named, Node, Positional, Symbol, TypeNode, name_occurrences }
+import v4.std.node {
+  Arrow,
+  Conj,
+  Edge,
+  Named,
+  Node,
+  Positional,
+  Symbol,
+  TypeNode,
+  arrow_body_edge,
+  name_occurrences
+}
 // 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: node-positional-child-targets — bind node://adhoc-sg2-positional-child-targets — dissolve-on-arrival: substrate canonical positional-child target projection on Node.children; lives in node_query (node.dag is import-free substrate root). forbidden: parallel edge-label filters outside std/node_query (e.g. translate-local conj_positional_targets folds).
 fn node_positional_child_targets(node: Node) -> List<Node> {
   fold(node.children, init: Empty, f: fn(acc, e) {
@@ -89,3 +100,54 @@ fn find_named_child(root: Node, name: Symbol) -> Outcome<Node> {
       })
   }
 }
+
+// 🟢 grounded — Arrow.body single-named-edge lookup (E-9); Conj-only find_named_child must not be reused on Arrow roots.
+fn find_arrow_body_child(root: Node) -> Outcome<Node> {
+  match root.kind {
+    TypeNode { connective: Arrow } =>
+      let count = name_occurrences(name: arrow_body_edge, children: root.children)
+      if count == 1 {
+        fold(
+          root.children,
+          init: outcome_rejected(d: Diagnostic {
+            reason: ^arrow_body_child_missing,
+            at: node_locus(node: root),
+            correction: Unavailable { reason: ExternalContractUnknown }
+          }),
+          f: fn(acc, e) {
+            match acc {
+              Accepted { value: _, diagnostics: _ } => acc
+              Rejected { diagnostics: _ } =>
+                match e.label {
+                  Named { name: edge_name } =>
+                    if edge_name == arrow_body_edge {
+                      outcome_accepted(value: e.target)
+                    } else {
+                      acc
+                    }
+                  Positional => acc
+                }
+            }
+          }
+        )
+      } else if count == 0 {
+        outcome_rejected(d: Diagnostic {
+          reason: ^arrow_body_child_missing,
+          at: node_locus(node: root),
+          correction: Unavailable { reason: ExternalContractUnknown }
+        })
+      } else {
+        outcome_rejected(d: Diagnostic {
+          reason: ^arrow_body_child_ambiguous,
+          at: node_locus(node: root),
+          correction: Unavailable { reason: ExternalContractUnknown }
+        })
+      }
+    _ =>
+      outcome_rejected(d: Diagnostic {
+        reason: ^arrow_body_child_not_arrow,
+        at: node_locus(node: root),
+        correction: Unavailable { reason: ExternalContractUnknown }
+      })
+  }
+}

src/v4/std/target_model.dag

@@ -51,6 +51,7 @@ import v4.std.find_witness {
 }
 import v4.std.node {
   Arrow,
+  ArrowBodyEdges,
   Atom,
   Cardinality,
   Conj,
@@ -3565,6 +3566,7 @@ fn type_expr_projection_child_slot_discipline_atom(connective: Connective) -> No
     NoEdges => target_type_expr_symbol_atom(id: target_type_expr_discipline_no_edges)
     LabeledEdges => target_type_expr_symbol_atom(id: target_type_expr_discipline_labeled)
     PositionalEdges => target_type_expr_symbol_atom(id: target_type_expr_discipline_positional)
+    ArrowBodyEdges => target_type_expr_symbol_atom(id: target_type_expr_discipline_positional)
     LoopBoundEdges => target_type_expr_symbol_atom(id: target_type_expr_discipline_positional)
   }
 }