distinct-node zip-fold predicate algebra body fill for coercion_fold (MVP-1 critical-path closer)

src/v4/std/coercion.dag

@@ -19,9 +19,7 @@ import v4.std.diagnostic {
   Outcome,
   Rejected,
   Unavailable,
-  diagnostics_singleton,
   outcome_rejected,
-  rejected_with_pending
 }
 import v4.std.find_witness {
   CandidateSet,
@@ -118,15 +116,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: fw.witness.evidence
+            }
+          }
+        },
+        diagnostics: fw_d
       }
     Rejected { diagnostics: r } => Rejected { diagnostics: r }
   }

src/v4/std/find_witness.dag

@@ -13,14 +13,20 @@ module v4.std.find_witness
 
 import v4.std.collection { List }
 import v4.std.diagnostic {
+  Accepted,
   Diagnostic,
   ExternalContractUnknown,
+  None,
   NodeLocus,
   Outcome,
+  Rejected,
   Unavailable,
   outcome_rejected
 }
-import v4.std.node { Node, Symbol }
+import v4.std.node {
+  Node,
+  Symbol
+}
 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
@@ -41,6 +47,11 @@ type FindWitnessResult {
   witness: StructuralPropertyWitness
   closedness: StructuralPropertyWitness
 }
+// 🟢 coproduct dissolution — local fold state for fail-closed unique candidate selection.
+type PassingCandidateFold
+  = NoPassingCandidate
+  | OnePassingCandidate { candidate: Node }
+  | ManyPassingCandidates
 // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
 type TargetSelectionPolicy
   = TargetDeclaredPriority { priority: Node }
@@ -70,19 +81,179 @@ fn find_witness_not_realized_diagnostic(source_facts: Node) -> Diagnostic {
     correction: Unavailable { reason: ExternalContractUnknown }
   }
 }
+fn exact_structural_equality_zip_fold(source_facts: Node, candidate: Node) -> Bool {
+  (source_facts.kind == candidate.kind)
+    && (count(source_facts.children) == count(candidate.children))
+}
+fn preservation_predicate_holds(
+  source_facts: Node,
+  candidate: Node,
+  predicate: PreservationPredicate,
+) -> Bool {
+  (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold)
+    && exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate)
+}
+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,
+) -> Outcome<Node> {
+  match fold(candidates.candidates, init: NoPassingCandidate, f: fn(acc, candidate) {
+    if preservation_predicate_holds(
+      source_facts: source_facts,
+      candidate: candidate,
+      predicate: predicate
+    ) {
+      match acc {
+        NoPassingCandidate => OnePassingCandidate { candidate: candidate }
+        OnePassingCandidate { candidate: _ } => ManyPassingCandidates
+        ManyPassingCandidates => ManyPassingCandidates
+      }
+    } else {
+      acc
+    }
+  }) {
+    NoPassingCandidate =>
+      outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts))
+    OnePassingCandidate { candidate: only } =>
+      Accepted { value: only, diagnostics: None }
+    ManyPassingCandidates =>
+      outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts))
+  }
+}
+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 => match only_passing_candidate(
+      source_facts: source_facts,
+      candidates: candidates,
+      predicate: predicate
+    ) {
+      Accepted { value: only, diagnostics: _ } => accepted_witness_result(
+        candidate: only,
+        candidates: candidates,
+        predicate: predicate
+      )
+      Rejected { diagnostics: r } => Rejected { diagnostics: r }
+    }
+    _ => 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) {
+    Accepted { value: witness, diagnostics: None }
+  } else {
+    outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts))
+  }
 }