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

src/v4/compiler/06_translate.dag

@@ -11,7 +11,8 @@
 // Consumes: compiler/04_infer.dag, compiler/00_compile.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.
 
 
@@ -20,6 +21,7 @@ module v4.compiler.translate
 
 import v4.compiler.compile { TargetModel, TargetSource }
 import v4.compiler.infer { InferredTree }
+import v4.std.collection { List }
 import v4.std.coercion {
   CoercionCandidateSet,
   CoercionResult,
@@ -176,8 +178,11 @@ fn target_selection_policy_from_model(target: TargetModel) -> Outcome<TargetSele
     }
   )
 }
+fn declared_inhabitant_candidates(inhabitants_root: Node) -> List<Node> {
+  map(inhabitants_root.children, fn(e) { e.target })
+}
 // `declared_inhabitants` edge names one closed candidate-set root Node on the target bundle;
-// find_witness enumerates inside that root when its body lands — not container-child traversal here.
+// translate flattens that root's children into the closed candidate list consumed by find_witness.
 fn coercion_candidates_from_target_model(
   target: TargetModel,
   closedness_evidence: Node
@@ -188,7 +193,7 @@ fn coercion_candidates_from_target_model(
       Accepted {
         value: CoercionCandidateSet {
           set: CandidateSet {
-            candidates: [inhabitants_root],
+            candidates: declared_inhabitant_candidates(inhabitants_root: inhabitants_root),
             closedness: StructuralPropertyWitness {
               property: target_model_edge_declared_inhabitants,
               evidence: closedness_evidence

src/v4/std/coercion.dag

@@ -19,22 +19,24 @@ import v4.std.diagnostic {
   Outcome,
   Rejected,
   Unavailable,
-  diagnostics_singleton,
-  outcome_rejected,
-  rejected_with_pending
+  outcome_rejected
 }
 import v4.std.find_witness {
   CandidateSet,
+  FindWitnessResult,
   PreservationPredicate,
   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 }
 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
@@ -104,6 +106,19 @@ fn declared_candidates_for_algebra(
     )
   )
 }
+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,15 +133,19 @@ 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 }
   }

src/v4/std/find_witness.dag

@@ -13,14 +13,16 @@ module v4.std.find_witness
 
 import v4.std.collection { List }
 import v4.std.diagnostic {
+  Accepted,
   Diagnostic,
   ExternalContractUnknown,
+  None,
   NodeLocus,
   Outcome,
   Unavailable,
   outcome_rejected
 }
-import v4.std.node { Node, Symbol }
+import v4.std.node { Node, Symbol, well_formed }
 import v4.std.witness { StructuralPropertyWitness }
 data find_witness_reason_no_candidate: Symbol = find_witness_reason_no_candidate
 data find_witness_reason_ambiguous_candidate: Symbol = find_witness_reason_ambiguous_candidate
@@ -70,19 +72,166 @@ fn find_witness_not_realized_diagnostic(source_facts: Node) -> Diagnostic {
     correction: Unavailable { reason: ExternalContractUnknown }
   }
 }
+// 🟡 coproduct dissolution — scaffold:exact-structural-preservation-identity-mvp · dissolve-on: W-T-10 structural zip-fold predicate algebra; exact_structural_equality accepts only source-identical Node evidence and other preservation rules fail closed.
+fn preservation_predicate_holds(
+  source_facts: Node,
+  candidate: Node,
+  predicate: PreservationPredicate,
+) -> Bool {
+  well_formed(n: source_facts)
+    && well_formed(n: predicate.algebra)
+    && well_formed(n: candidate)
+    && (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold)
+    && (predicate.algebra == source_facts)
+    && (candidate == source_facts)
+}
+fn passing_candidate_count(
+  source_facts: Node,
+  candidates: CandidateSet,
+  predicate: PreservationPredicate,
+) -> Int {
+  fold(candidates.candidates, init: 0, f: fn(acc, candidate) {
+    if preservation_predicate_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      predicate: predicate
+    ) {
+      acc + 1
+    } else {
+      acc
+    }
+  })
+}
+fn only_passing_candidate(
+  source_facts: Node,
+  candidates: CandidateSet,
+  predicate: PreservationPredicate,
+) -> Node {
+  fold(candidates.candidates, init: source_facts, f: fn(acc, candidate) {
+    if preservation_predicate_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      predicate: predicate
+    ) {
+      candidate
+    } else {
+      acc
+    }
+  })
+}
+fn selected_candidate_count(
+  source_facts: Node,
+  candidates: CandidateSet,
+  predicate: PreservationPredicate,
+  selection: Node,
+) -> Int {
+  fold(candidates.candidates, init: 0, f: fn(acc, candidate) {
+    if (candidate == selection) && preservation_predicate_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      predicate: predicate
+    ) {
+      acc + 1
+    } else {
+      acc
+    }
+  })
+}
+fn accepted_witness_result(
+  candidate: Node,
+  candidates: CandidateSet,
+  predicate: PreservationPredicate,
+) -> Outcome<FindWitnessResult> {
+  Accepted {
+    value: FindWitnessResult {
+      candidate: candidate,
+      witness: StructuralPropertyWitness {
+        property: predicate.preservation_rule,
+        evidence: candidate
+      },
+      closedness: candidates.closedness
+    },
+    diagnostics: None
+  }
+}
+fn resolve_selected_candidate(
+  source_facts: Node,
+  candidates: CandidateSet,
+  predicate: PreservationPredicate,
+  selection: Node,
+) -> Outcome<FindWitnessResult> {
+  match selected_candidate_count(
+    source_facts: source_facts,
+    candidates: candidates,
+    predicate: predicate,
+    selection: selection
+  ) {
+    1 => accepted_witness_result(
+      candidate: selection,
+      candidates: candidates,
+      predicate: predicate
+    )
+    0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts))
+    _ => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts))
+  }
+}
 fn find_witness(
   source_facts: Node,
   candidates: CandidateSet,
   predicate: PreservationPredicate,
   multiplicity_policy: MultiplicityPolicy,
 ) -> Outcome<FindWitnessResult> {
-  outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
+  let passing_count = passing_candidate_count(
+    source_facts: source_facts,
+    candidates: candidates,
+    predicate: predicate
+  )
+  match passing_count {
+    0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts))
+    1 => accepted_witness_result(
+      candidate: only_passing_candidate(
+        source_facts: source_facts,
+        candidates: candidates,
+        predicate: predicate
+      ),
+      candidates: candidates,
+      predicate: predicate
+    )
+    _ => match multiplicity_policy {
+      UniqueOnly =>
+        outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts))
+      TargetSelection { policy: p } => match p {
+        TargetDeclaredPriority { priority: priority } =>
+          resolve_selected_candidate(
+            source_facts: source_facts,
+            candidates: candidates,
+            predicate: predicate,
+            selection: priority
+          )
+        UserSelected { selection: selection } =>
+          resolve_selected_candidate(
+            source_facts: source_facts,
+            candidates: candidates,
+            predicate: predicate,
+            selection: selection
+          )
+      }
+    }
+  }
 }
 fn verify_witness(
   source_facts: Node,
   candidate: Node,
   predicate: PreservationPredicate,
   witness: StructuralPropertyWitness,
 ) -> Outcome<StructuralPropertyWitness> {
-  outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts))
+  if preservation_predicate_holds(
+    source_facts: source_facts,
+    candidate: candidate,
+    predicate: predicate
+  ) && (witness.property == predicate.preservation_rule) && (witness.evidence == candidate) {
+    Accepted { value: witness, diagnostics: None }
+  } else {
+    outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts))
+  }
 }

src/v4/test/claim/manual/mvp1_rust_add_translate.dag

@@ -2,7 +2,7 @@
 // Scope: MVP-1 T-10 receipt — structural TestClaim anchors for translate/emit substrate.
 // Owns: mvp_add_arrow_node, claim_mvp1_translate_module_compiles, claim_mvp1_emit_module_compiles.
 // Consumes: compiler/05_emit.dag, compiler/06_translate.dag, std/verification.dag, std/diagnostic.dag, std/node.dag.
-// Status: parse-surface receipt; full InferredTree(add)->Accepted emit blocked on std/find_witness body.
+// Status: parse-surface receipt; full InferredTree(add)->Accepted emit remains blocked on compiler-stage canonical grounding and target serialization scaffolds.
 // Anchor: docs/design-v4-compiler-homomorphism.md MVP-1 worked example.