diff --git a/src/v4/compiler/03_body_producer.dag b/src/v4/compiler/03_body_producer.dag new file mode 100644 index 00000000000..83c661b1fc4 --- /dev/null +++ b/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 { + 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 { + 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 { + 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 + } +} diff --git a/src/v4/std/node.dag b/src/v4/std/node.dag index 250cec5ba96..57f923e16db 100644 --- a/src/v4/std/node.dag +++ b/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 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 @@ -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,8 +151,7 @@ fn name_occurrences(name: Symbol, children: List) -> 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) -> Int { +fn positional_child_count(children: List) -> Int { fold(children, init: 0, f: fn(acc, e) { match e.label { Positional => acc + 1 @@ -156,6 +159,10 @@ fn loop_positional_child_count(children: List) -> 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) -> 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) -> Bool { fold(children, init: true, f: fn(acc, e) { @@ -172,6 +179,21 @@ fn loop_behavior_edges_conform(children: List) -> 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) -> 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) -> 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, 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, 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) -> List { + filter(children, e => match e.label { Positional => true, Named { name: _ } => false }) +} +fn arrow_body_edges_for_content_hash(children: List) -> List { + 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) -> List { + 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) -> List { + 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) -> List { 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, diff --git a/src/v4/std/node_query.dag b/src/v4/std/node_query.dag index 88f8a4671ba..75a4ffe4ad0 100644 --- a/src/v4/std/node_query.dag +++ b/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 { fold(node.children, init: Empty, f: fn(acc, e) { @@ -89,3 +100,54 @@ fn find_named_child(root: Node, name: Symbol) -> Outcome { }) } } + +// 🟢 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 { + 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 } + }) + } +} diff --git a/src/v4/std/target_model.dag b/src/v4/std/target_model.dag index c3a8698d93c..68e1c373504 100644 --- a/src/v4/std/target_model.dag +++ b/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) } } diff --git a/src/v4/test/claim/manual/comprep_add_body_producer.dag b/src/v4/test/claim/manual/comprep_add_body_producer.dag new file mode 100644 index 00000000000..fee1ec053b7 --- /dev/null +++ b/src/v4/test/claim/manual/comprep_add_body_producer.dag @@ -0,0 +1,132 @@ +// src/v4/test/claim/manual/comprep_add_body_producer.dag +// Scope: COMPREP wave-1 keystone receipt — body producer attaches Behavior sub-DAG on Arrow.body. +// Status: producer well-formedness + discriminating body-shape witness (operand order flips attachment). + +module v4.test.claim.manual.comprep_add_body_producer + +import v4.compiler.body_producer { + arrow_has_body_edge, + produce_mvp1_add_arrow_with_body, + produce_mvp1_add_binary_body +} +import v4.std.diagnostic { Accepted, Rejected } +import v4.std.logic { Bool } +import v4.std.node { + Atom, + ComputationNode, + Edge, + Named, + Node, + Positional, + Transform, + TypeNode, + arrow_body_edge, + well_formed +} +import v4.std.node_query { find_arrow_body_child } +import v4.std.verification { + EqualsClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Unit, + manual_claim_anchor +} + +fn comprep_bool_node(pass: Bool) -> Node { + if pass { + Node { + kind: TypeNode { connective: Atom { identity: ^comprep_body_producer_pass } }, + children: [] + } + } else { + Node { + kind: TypeNode { connective: Atom { identity: ^comprep_body_producer_fail } }, + children: [] + } + } +} + +fn comprep_produce_add_arrow_accepts() -> Bool { + match produce_mvp1_add_arrow_with_body() { + Accepted { value: arrow, diagnostics: _ } => + well_formed(n: arrow) && arrow_has_body_edge(arrow: arrow) + Rejected { diagnostics: _ } => false + } +} + +// Discriminating red: swap operand param refs — body subtree changes, well-formedness holds. +fn comprep_swapped_operand_body() -> Node { + Node { + kind: ComputationNode { behavior: Transform }, + children: [ + Edge { + label: Positional, + target: Node { + kind: TypeNode { connective: Atom { identity: ^dag_token_plus } }, + children: [] + } + }, + Edge { + label: Positional, + target: Node { + kind: TypeNode { connective: Atom { identity: ^dag_binding_param_y } }, + children: [] + } + }, + Edge { + label: Positional, + target: Node { + kind: TypeNode { connective: Atom { identity: ^dag_binding_param_x } }, + children: [] + } + } + ] + } +} + +fn comprep_body_operand_order_differs() -> Bool { + let canonical = produce_mvp1_add_binary_body() + let swapped = comprep_swapped_operand_body() + canonical != swapped +} + +fn comprep_body_edge_targets_binary_transform() -> Bool { + match produce_mvp1_add_arrow_with_body() { + Accepted { value: arrow, diagnostics: _ } => + match find_arrow_body_child(root: arrow) { + Accepted { value: body, diagnostics: _ } => + match body.kind { + ComputationNode { behavior: Transform } => true + _ => false + } + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +data claim_comprep_add_body_producer_well_formed: TestClaim = EqualsClaim { + label: "manual/comprep: produce_mvp1_add_arrow_with_body is well-formed with Arrow.body Behavior subtree", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: comprep_bool_node(pass: comprep_produce_add_arrow_accepts()), + rhs: comprep_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_comprep_add_body_operand_order_discriminates: TestClaim = EqualsClaim { + label: "manual/comprep: swapped operand param refs change body subtree (discriminating red for eval follow-up)", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: comprep_bool_node(pass: comprep_body_operand_order_differs()), + rhs: comprep_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_comprep_add_body_is_transform: TestClaim = EqualsClaim { + label: "manual/comprep: Arrow.body target is ComputationNode Transform for MVP add", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: comprep_bool_node(pass: comprep_body_edge_targets_binary_transform()), + rhs: comprep_bool_node(pass: true), + classification: TestClassification { tier: Tier1, layer: Unit } +}