Wave-4-A — find_witness enumeration and coercion_fold identity-MVP body fill

src/v4/compiler/06_translate.dag

@@ -1,15 +1,18 @@
 // src/v4/compiler/06_translate.dag
 // Scope: Stage 5a — T-10 surface + fail-closed staging (not live translate on InferredTree yet).
-// Owns: TargetNodeTree, TargetBundleChildLookup, target_bundle_child, target_bundle_child_lookup_step,
-//       target_selection_policy_from_model, coercion_candidates_from_target_model,
+// Owns: TargetNodeTree, TargetBundleChildLookup, target_model_edge_selection_policy,
+//       target_model_edge_declared_inhabitants, target_model_edge_serialize_emitted,
+//       target_model_edge_serialize_source, target_bundle_child, target_bundle_child_lookup_step,
+//       target_selection_priority_from_model, coercion_candidates_from_target_model,
 //       target_serialize_source_from_model, translate_target_source_not_realized,
 //       translate_canonical_grounding_not_realized, canonical_grounding_for_node,
 //       coerce_grounded_node, translate_fold_init, translate_fold_step,
 //       translate_node, translate.
 // Consumes: compiler/04_infer.dag, compiler/07_target_carriers.dag, std/coercion.dag, std/constraints.dag,
 //           std/find_witness.dag, std/diagnostic.dag, std/node.dag, std/witness.dag, std/collection.dag.
 // Status: W-T-10-impl staging — fold_node + coercion_fold call-shape; canonical_grounding and
-// coercion_fold bodies fail closed until T-9 (#3464) + find_witness + T-4 rust.dag land.
+// coercion_fold now delegates to find_witness; translate still fails closed where canonical grounding
+// or target serialization scaffolds lack substrate facts.
 // Anchor: docs/design-v4-compiler-homomorphism.md Stage 5a; Ratified Q14.
 
 
@@ -21,7 +24,9 @@ import v4.compiler.infer { InferredTree }
 import v4.std.coercion {
   CoercionCandidateSet,
   CoercionResult,
-  coercion_fold
+  coercion_candidate_set_from_declared_inhabitants,
+  coercion_fold,
+  coercion_fold_with_declared_priority
 }
 import v4.std.constraints { CanonicalGrounding }
 import v4.std.diagnostic {
@@ -39,11 +44,7 @@ import v4.std.diagnostic {
   outcome_rejected,
   rejected_with_pending
 }
-import v4.std.find_witness {
-  CandidateSet,
-  TargetDeclaredPriority,
-  TargetSelectionPolicy
-}
+import v4.std.find_witness { CandidateSet }
 import v4.std.node {
   Conj,
   Edge,
@@ -166,40 +167,29 @@ fn target_bundle_child(target: TargetModel, edge_name: Symbol) -> Outcome<Node>
       outcome_rejected(translate_target_bundle_malformed_diagnostic(target: target))
   }
 }
-fn target_selection_policy_from_model(target: TargetModel) -> Outcome<TargetSelectionPolicy> {
+fn target_selection_priority_from_model(target: TargetModel) -> Outcome<Node> {
   bind_outcome(
     o: target_bundle_child(target: target, edge_name: target_model_edge_selection_policy),
     f: fn(priority_node) {
       Accepted {
-        value: TargetDeclaredPriority { priority: priority_node },
+        value: priority_node,
         diagnostics: None
       }
     }
   )
 }
-// `declared_inhabitants` edge supplies one Conj root; staging passes it as the sole
-// `CandidateSet.candidates` entry (aggregate root — see find_witness body, W-T-10).
-// Per-primitive inhabitants are named children of that Conj; enumeration inside the root
-// is not performed in this translate staging path yet.
+// `declared_inhabitants` edge names one closed candidate-set root Node on the target bundle;
+// std/coercion constructs the closed candidate list consumed by find_witness.
 fn coercion_candidates_from_target_model(
-  target: TargetModel,
-  closedness_evidence: Node
+  target: TargetModel
 ) -> Outcome<CoercionCandidateSet> {
   bind_outcome(
     o: target_bundle_child(target: target, edge_name: target_model_edge_declared_inhabitants),
     f: fn(inhabitants_root) {
-      Accepted {
-        value: CoercionCandidateSet {
-          set: CandidateSet {
-            candidates: [inhabitants_root],
-            closedness: StructuralPropertyWitness {
-              property: target_model_edge_declared_inhabitants,
-              evidence: closedness_evidence
-            }
-          }
-        },
-        diagnostics: None
-      }
+      coercion_candidate_set_from_declared_inhabitants(
+        inhabitants_root: inhabitants_root,
+        closedness_property: target_model_edge_declared_inhabitants
+      )
     }
   )
 }
@@ -217,18 +207,17 @@ fn coerce_grounded_node(
     o: canonical_grounding_for_node(tree: tree, node: source),
     f: fn(grounding) {
       bind_outcome(
-        o: target_selection_policy_from_model(target: target),
-        f: fn(policy) {
+        o: target_selection_priority_from_model(target: target),
+        f: fn(priority) {
           bind_outcome(
             o: coercion_candidates_from_target_model(
-              target: target,
-              closedness_evidence: grounding.node
+              target: target
             ),
             f: fn(candidates) {
-              coercion_fold(
+              coercion_fold_with_declared_priority(
                 source: grounding,
                 candidates: candidates,
-                policy: policy
+                priority: priority
               )
             }
           )

src/v4/std/coercion.dag

@@ -10,37 +10,43 @@
 module v4.std.coercion
 
 
+import v4.std.collection { List }
 import v4.std.constraints { CanonicalGrounding, CanonicalGroundingWitness }
 import v4.std.diagnostic {
   Accepted,
   Diagnostic,
   ExternalContractUnknown,
+  None,
   NodeLocus,
   Outcome,
   Rejected,
   Unavailable,
-  diagnostics_singleton,
-  outcome_rejected,
-  rejected_with_pending
+  outcome_rejected
 }
 import v4.std.find_witness {
   CandidateSet,
+  FindWitnessResult,
   PreservationPredicate,
+  TargetDeclaredPriority,
   TargetSelection,
   TargetSelectionPolicy,
   find_witness,
   preservation_rule_exact_structural_equality_zip_fold
 }
-import v4.std.node { Node, Symbol }
+import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed }
 import v4.std.witness { HomomorphismWitness, StructuralPropertyWitness }
 data coercion_property_closed_candidate_set: Symbol = coercion_property_closed_candidate_set
 data coercion_property_candidate_set_closedness: Symbol = coercion_property_candidate_set_closedness
+data coercion_homomorphism_evidence_source: Symbol = coercion_homomorphism_evidence_source
+data coercion_homomorphism_evidence_candidate: Symbol = coercion_homomorphism_evidence_candidate
+data coercion_homomorphism_evidence_find_witness: Symbol = coercion_homomorphism_evidence_find_witness
 data homomorphism_rule_exact_structural_equality: Symbol = homomorphism_rule_exact_structural_equality
 data coercion_not_realized: Symbol = coercion_not_realized
 data coercion_mismatch_no_target: Symbol = coercion_mismatch_no_target
 data coercion_mismatch_ambiguous: Symbol = coercion_mismatch_ambiguous
 data coercion_mismatch_structural: Symbol = coercion_mismatch_structural
 data coercion_mismatch_would_lose: Symbol = coercion_mismatch_would_lose
+data coercion_mismatch_candidate_set_not_closed: Symbol = coercion_mismatch_candidate_set_not_closed
 // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
 type CoercionQuality
   = Identity
@@ -104,6 +110,52 @@ fn declared_candidates_for_algebra(
     )
   )
 }
+fn declared_inhabitant_candidates(inhabitants_root: Node) -> List<Node> {
+  map(inhabitants_root.children, fn(e) { e.target })
+}
+fn coercion_candidate_set_not_closed_diagnostic(inhabitants_root: Node) -> Diagnostic {
+  Diagnostic {
+    reason: coercion_mismatch_candidate_set_not_closed,
+    at: NodeLocus { node: inhabitants_root },
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+fn coercion_candidate_set_from_declared_inhabitants(
+  inhabitants_root: Node,
+  closedness_property: Symbol,
+) -> Outcome<CoercionCandidateSet> {
+  if well_formed(n: inhabitants_root) {
+    Accepted {
+      value: CoercionCandidateSet {
+        set: CandidateSet {
+          candidates: declared_inhabitant_candidates(inhabitants_root: inhabitants_root),
+          closedness: StructuralPropertyWitness {
+            property: closedness_property,
+            evidence: inhabitants_root
+          }
+        }
+      },
+      diagnostics: None
+    }
+  } else {
+    outcome_rejected(
+      coercion_candidate_set_not_closed_diagnostic(inhabitants_root: inhabitants_root)
+    )
+  }
+}
+fn coercion_homomorphism_evidence(
+  source: CanonicalGrounding,
+  fw: FindWitnessResult,
+) -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [
+      Edge { label: Named { name: coercion_homomorphism_evidence_source }, target: source.node },
+      Edge { label: Named { name: coercion_homomorphism_evidence_candidate }, target: fw.candidate },
+      Edge { label: Named { name: coercion_homomorphism_evidence_find_witness }, target: fw.witness.evidence }
+    ]
+  }
+}
 fn coercion_fold(
   source: CanonicalGrounding,
   candidates: CoercionCandidateSet,
@@ -118,16 +170,31 @@ fn coercion_fold(
     },
     multiplicity_policy: TargetSelection { policy: policy }
   ) {
-    // Scaffold only while find_witness rejects: W-T-10 must lift FindWitnessResult → CoercionResult here.
-    Accepted { value: _, diagnostics: fw_d } =>
-      Rejected {
-        diagnostics: rejected_with_pending(
-          pending: fw_d,
-          rejected: diagnostics_singleton(
-            d: coercion_not_realized_diagnostic(source: source, kind: NoTargetCandidate)
-          )
-        )
+    Accepted { value: fw, diagnostics: fw_d } =>
+      Accepted {
+        value: CoercionResult {
+          target: fw.candidate,
+          quality: if fw.candidate == source.node { Identity } else { Exact },
+          witness: CoercionWitness {
+            homomorphism: HomomorphismWitness {
+              rule: homomorphism_rule_exact_structural_equality,
+              evidence: coercion_homomorphism_evidence(source: source, fw: fw)
+            }
+          }
+        },
+        diagnostics: fw_d
       }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
   }
 }
+fn coercion_fold_with_declared_priority(
+  source: CanonicalGrounding,
+  candidates: CoercionCandidateSet,
+  priority: Node,
+) -> Outcome<CoercionResult> {
+  coercion_fold(
+    source: source,
+    candidates: candidates,
+    policy: TargetDeclaredPriority { priority: priority }
+  )
+}