From 8f6c709af8ebc03f94d49ba1987e2612ac599c38 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:10:19 -0400 Subject: [PATCH 01/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/coercion.dag | 24 ++--- src/v4/std/find_witness.dag | 191 +++++++++++++++++++++++++++++++++++- 2 files changed, 201 insertions(+), 14 deletions(-) diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag index 2d3fe124ed1..ef1c317efa6 100644 --- a/src/v4/std/coercion.dag +++ b/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: Exact, + witness: CoercionWitness { + homomorphism: HomomorphismWitness { + rule: homomorphism_rule_exact_structural_equality, + evidence: fw.witness.evidence + } + } + }, + diagnostics: fw_d } Rejected { diagnostics: r } => Rejected { diagnostics: r } } diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 725afb4d8dc..07860aa25e6 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -13,12 +13,16 @@ module v4.std.find_witness import v4.std.collection { List } import v4.std.diagnostic { + Accepted, Diagnostic, + Diagnostics, ExternalContractUnknown, NodeLocus, Outcome, + Rejected, Unavailable, - outcome_rejected + outcome_rejected, + outcome_with_diagnostics } import v4.std.node { Node, Symbol } import v4.std.witness { StructuralPropertyWitness } @@ -41,6 +45,10 @@ type FindWitnessResult { witness: StructuralPropertyWitness closedness: StructuralPropertyWitness } +type PassingCandidates { + matches: List + count: Int +} // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. type TargetSelectionPolicy = TargetDeclaredPriority { priority: Node } @@ -70,13 +78,182 @@ 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 == candidate +} +fn preservation_predicate_holds( + source_facts: Node, + candidate: Node, + predicate: PreservationPredicate, +) -> Bool { + if predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold { + exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate) + } else { + false + } +} +fn find_witness_result_for_candidate( + candidate: Node, + predicate: PreservationPredicate, + closedness: StructuralPropertyWitness, +) -> FindWitnessResult { + FindWitnessResult { + candidate: candidate, + witness: StructuralPropertyWitness { + property: predicate.preservation_rule, + evidence: candidate + }, + closedness: closedness + } +} +fn passing_candidates_step( + acc: PassingCandidates, + source_facts: Node, + predicate: PreservationPredicate, + closedness: StructuralPropertyWitness, + candidate: Node, +) -> PassingCandidates { + if preservation_predicate_holds( + source_facts: source_facts, + candidate: candidate, + predicate: predicate + ) { + PassingCandidates { + matches: list_push( + acc.matches, + find_witness_result_for_candidate( + candidate: candidate, + predicate: predicate, + closedness: closedness + ) + ), + count: acc.count + 1 + } + } else { + acc + } +} +fn passing_candidates_for( + source_facts: Node, + candidates: CandidateSet, + predicate: PreservationPredicate, +) -> PassingCandidates { + fold( + candidates.candidates, + init: PassingCandidates { matches: [], count: 0 }, + f: fn(acc, candidate) { + passing_candidates_step( + acc: acc, + source_facts: source_facts, + predicate: predicate, + closedness: candidates.closedness, + candidate: candidate + ) + } + ) +} +fn accepted_find_witness_result( + result: FindWitnessResult, + diagnostics: Diagnostics, +) -> Outcome { + outcome_with_diagnostics(value: result, diagnostics: diagnostics) +} +fn only_passing_result( + source_facts: Node, + passing: PassingCandidates, + diagnostics: Diagnostics, +) -> Outcome { + match passing.matches { + Empty => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) + Cons { head: result, tail: _ } => accepted_find_witness_result(result: result, diagnostics: diagnostics) + } +} +fn target_selection_filter_step( + acc: PassingCandidates, + selection: Node, + result: FindWitnessResult, +) -> PassingCandidates { + if result.candidate == selection { + PassingCandidates { + matches: list_push(acc.matches, result), + count: acc.count + 1 + } + } else { + acc + } +} +fn target_selection_matches( + passing: PassingCandidates, + selection: Node, +) -> PassingCandidates { + fold( + passing.matches, + init: PassingCandidates { matches: [], count: 0 }, + f: fn(acc, result) { + target_selection_filter_step(acc: acc, selection: selection, result: result) + } + ) +} +fn resolve_target_selection( + source_facts: Node, + passing: PassingCandidates, + selection: Node, + diagnostics: Diagnostics, +) -> Outcome { + let selected = target_selection_matches(passing: passing, selection: selection) + match selected.count { + 1 => only_passing_result(source_facts: source_facts, passing: selected, diagnostics: diagnostics) + _ => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + } +} +fn resolve_multiple_passing( + source_facts: Node, + passing: PassingCandidates, + multiplicity_policy: MultiplicityPolicy, + diagnostics: Diagnostics, +) -> Outcome { + match multiplicity_policy { + UniqueOnly => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + TargetSelection { policy } => match policy { + TargetDeclaredPriority { priority } => + resolve_target_selection( + source_facts: source_facts, + passing: passing, + selection: priority, + diagnostics: diagnostics + ) + UserSelected { selection } => + resolve_target_selection( + source_facts: source_facts, + passing: passing, + selection: selection, + diagnostics: diagnostics + ) + } + } +} fn find_witness( source_facts: Node, candidates: CandidateSet, predicate: PreservationPredicate, multiplicity_policy: MultiplicityPolicy, ) -> Outcome { - outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts)) + let passing = passing_candidates_for( + source_facts: source_facts, + candidates: candidates, + predicate: predicate + ) + match passing.count { + 0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) + 1 => only_passing_result(source_facts: source_facts, passing: passing, diagnostics: None) + _ => + resolve_multiple_passing( + source_facts: source_facts, + passing: passing, + multiplicity_policy: multiplicity_policy, + diagnostics: None + ) + } } fn verify_witness( source_facts: Node, @@ -84,5 +261,13 @@ fn verify_witness( predicate: PreservationPredicate, witness: StructuralPropertyWitness, ) -> Outcome { - 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)) + } } From 1d5cb3cc679f3b4b52bc3bc9c63c0105d30d2b5a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:14:49 -0400 Subject: [PATCH 02/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 207 +++++++++++++++++++++++++++++++++++- 1 file changed, 202 insertions(+), 5 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 07860aa25e6..08f5f6367fc 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -19,7 +19,6 @@ import v4.std.diagnostic { ExternalContractUnknown, NodeLocus, Outcome, - Rejected, Unavailable, outcome_rejected, outcome_with_diagnostics @@ -45,8 +44,13 @@ type FindWitnessResult { witness: StructuralPropertyWitness closedness: StructuralPropertyWitness } +// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. +type PassingSelection + = NoPassing + | OnePassing { result: FindWitnessResult } + | MultiplePassing type PassingCandidates { - matches: List + selection: PassingSelection count: Int } // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. @@ -119,9 +123,202 @@ fn passing_candidates_step( predicate: predicate ) { PassingCandidates { - matches: list_push( - acc.matches, - find_witness_result_for_candidate( + selection: match acc.selection { + NoPassing => + OnePassing { + result: find_witness_result_for_candidate( + candidate: candidate, + predicate: predicate, + closedness: closedness + ) + } + OnePassing { result: _ } => MultiplePassing + MultiplePassing => MultiplePassing + }, + count: acc.count + 1 + } + } else { + acc + } +} +fn selected_candidate_step( + acc: PassingCandidates, + source_facts: Node, + predicate: PreservationPredicate, + closedness: StructuralPropertyWitness, + selection: Node, + candidate: Node, +) -> PassingCandidates { + if (candidate == selection) && preservation_predicate_holds( + source_facts: source_facts, + candidate: candidate, + predicate: predicate + ) { + PassingCandidates { + selection: match acc.selection { + NoPassing => + OnePassing { + result: find_witness_result_for_candidate( + candidate: candidate, + predicate: predicate, + closedness: closedness + ) + } + OnePassing { result: _ } => MultiplePassing + MultiplePassing => MultiplePassing + }, + count: acc.count + 1 + } + } else { + acc + } +} +fn selected_passing_candidates_for( + source_facts: Node, + candidates: CandidateSet, + predicate: PreservationPredicate, + selection: Node, +) -> PassingCandidates { + fold( + candidates.candidates, + init: PassingCandidates { selection: NoPassing, count: 0 }, + f: fn(acc, candidate) { + selected_candidate_step( + acc: acc, + source_facts: source_facts, + predicate: predicate, + closedness: candidates.closedness, + selection: selection, + candidate: candidate + ) + } + ) +} +fn passing_candidates_for( + source_facts: Node, + candidates: CandidateSet, + predicate: PreservationPredicate, +) -> PassingCandidates { + fold( + candidates.candidates, + init: PassingCandidates { selection: NoPassing, count: 0 }, + f: fn(acc, candidate) { + passing_candidates_step( + acc: acc, + source_facts: source_facts, + predicate: predicate, + closedness: candidates.closedness, + candidate: candidate + ) + } + ) +} +fn accepted_find_witness_result( + result: FindWitnessResult, + diagnostics: Diagnostics, +) -> Outcome { + outcome_with_diagnostics(value: result, diagnostics: diagnostics) +} +fn only_passing_result( + source_facts: Node, + passing: PassingCandidates, + diagnostics: Diagnostics, +) -> Outcome { + match passing.selection { + OnePassing { result } => accepted_find_witness_result(result: result, diagnostics: diagnostics) + NoPassing => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) + MultiplePassing => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + } +} +fn resolve_target_selection( + source_facts: Node, + candidates: CandidateSet, + predicate: PreservationPredicate, + selection: Node, + diagnostics: Diagnostics, +) -> Outcome { + let selected = selected_passing_candidates_for( + source_facts: source_facts, + candidates: candidates, + predicate: predicate, + selection: selection + ) + match selected.count { + 1 => only_passing_result(source_facts: source_facts, passing: selected, diagnostics: diagnostics) + _ => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + } +} +fn resolve_multiple_passing( + source_facts: Node, + candidates: CandidateSet, + passing: PassingCandidates, + predicate: PreservationPredicate, + multiplicity_policy: MultiplicityPolicy, + diagnostics: Diagnostics, +) -> Outcome { + match multiplicity_policy { + UniqueOnly => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + TargetSelection { policy } => match policy { + TargetDeclaredPriority { priority } => + resolve_target_selection( + source_facts: source_facts, + candidates: candidates, + predicate: predicate, + selection: priority, + diagnostics: diagnostics + ) + UserSelected { selection } => + resolve_target_selection( + source_facts: source_facts, + candidates: candidates, + predicate: predicate, + selection: selection, + diagnostics: diagnostics + ) + } + } +} +fn find_witness( + source_facts: Node, + candidates: CandidateSet, + predicate: PreservationPredicate, + multiplicity_policy: MultiplicityPolicy, +) -> Outcome { + let passing = passing_candidates_for( + source_facts: source_facts, + candidates: candidates, + predicate: predicate + ) + match passing.count { + 0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) + 1 => only_passing_result(source_facts: source_facts, passing: passing, diagnostics: None) + _ => + resolve_multiple_passing( + source_facts: source_facts, + candidates: candidates, + passing: passing, + predicate: predicate, + multiplicity_policy: multiplicity_policy, + diagnostics: None + ) + } +} +fn verify_witness( + source_facts: Node, + candidate: Node, + predicate: PreservationPredicate, + witness: StructuralPropertyWitness, +) -> Outcome { + 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)) + } +} candidate: candidate, predicate: predicate, closedness: closedness From 65631a8617f93e8ec108c4a2b02d3d98c7cd3085 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:16:27 -0400 Subject: [PATCH 03/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 149 ------------------------------------ 1 file changed, 149 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 08f5f6367fc..9b3f868fb0b 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -303,155 +303,6 @@ fn find_witness( ) } } -fn verify_witness( - source_facts: Node, - candidate: Node, - predicate: PreservationPredicate, - witness: StructuralPropertyWitness, -) -> Outcome { - 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)) - } -} - candidate: candidate, - predicate: predicate, - closedness: closedness - ) - ), - count: acc.count + 1 - } - } else { - acc - } -} -fn passing_candidates_for( - source_facts: Node, - candidates: CandidateSet, - predicate: PreservationPredicate, -) -> PassingCandidates { - fold( - candidates.candidates, - init: PassingCandidates { matches: [], count: 0 }, - f: fn(acc, candidate) { - passing_candidates_step( - acc: acc, - source_facts: source_facts, - predicate: predicate, - closedness: candidates.closedness, - candidate: candidate - ) - } - ) -} -fn accepted_find_witness_result( - result: FindWitnessResult, - diagnostics: Diagnostics, -) -> Outcome { - outcome_with_diagnostics(value: result, diagnostics: diagnostics) -} -fn only_passing_result( - source_facts: Node, - passing: PassingCandidates, - diagnostics: Diagnostics, -) -> Outcome { - match passing.matches { - Empty => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) - Cons { head: result, tail: _ } => accepted_find_witness_result(result: result, diagnostics: diagnostics) - } -} -fn target_selection_filter_step( - acc: PassingCandidates, - selection: Node, - result: FindWitnessResult, -) -> PassingCandidates { - if result.candidate == selection { - PassingCandidates { - matches: list_push(acc.matches, result), - count: acc.count + 1 - } - } else { - acc - } -} -fn target_selection_matches( - passing: PassingCandidates, - selection: Node, -) -> PassingCandidates { - fold( - passing.matches, - init: PassingCandidates { matches: [], count: 0 }, - f: fn(acc, result) { - target_selection_filter_step(acc: acc, selection: selection, result: result) - } - ) -} -fn resolve_target_selection( - source_facts: Node, - passing: PassingCandidates, - selection: Node, - diagnostics: Diagnostics, -) -> Outcome { - let selected = target_selection_matches(passing: passing, selection: selection) - match selected.count { - 1 => only_passing_result(source_facts: source_facts, passing: selected, diagnostics: diagnostics) - _ => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) - } -} -fn resolve_multiple_passing( - source_facts: Node, - passing: PassingCandidates, - multiplicity_policy: MultiplicityPolicy, - diagnostics: Diagnostics, -) -> Outcome { - match multiplicity_policy { - UniqueOnly => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) - TargetSelection { policy } => match policy { - TargetDeclaredPriority { priority } => - resolve_target_selection( - source_facts: source_facts, - passing: passing, - selection: priority, - diagnostics: diagnostics - ) - UserSelected { selection } => - resolve_target_selection( - source_facts: source_facts, - passing: passing, - selection: selection, - diagnostics: diagnostics - ) - } - } -} -fn find_witness( - source_facts: Node, - candidates: CandidateSet, - predicate: PreservationPredicate, - multiplicity_policy: MultiplicityPolicy, -) -> Outcome { - let passing = passing_candidates_for( - source_facts: source_facts, - candidates: candidates, - predicate: predicate - ) - match passing.count { - 0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) - 1 => only_passing_result(source_facts: source_facts, passing: passing, diagnostics: None) - _ => - resolve_multiple_passing( - source_facts: source_facts, - passing: passing, - multiplicity_policy: multiplicity_policy, - diagnostics: None - ) - } -} fn verify_witness( source_facts: Node, candidate: Node, From b72b0f69adfa3ed5fcf38788065dbeaa2cb62a63 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:18:01 -0400 Subject: [PATCH 04/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 73 +++++++++++++++++++++++++++++++++---- 1 file changed, 66 insertions(+), 7 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 9b3f868fb0b..99398d5831d 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -17,19 +17,38 @@ import v4.std.diagnostic { Diagnostic, Diagnostics, ExternalContractUnknown, + None, NodeLocus, Outcome, Unavailable, outcome_rejected, outcome_with_diagnostics } -import v4.std.node { Node, Symbol } +import v4.std.node { + Atom, + Cardinality, + ComputationNode, + Conj, + Connective, + Disj, + Edge, + Arrow, + Instantiation, + Node, + NodeFold, + NodeKind, + Symbol, + TypeNode, + fold_node, + 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 data find_witness_reason_not_realized: Symbol = find_witness_reason_not_realized data preservation_rule_constraint_satisfaction: Symbol = preservation_rule_constraint_satisfaction data preservation_rule_exact_structural_equality_zip_fold: Symbol = preservation_rule_exact_structural_equality_zip_fold +data exact_structural_zip_fold_atom: Symbol = exact_structural_zip_fold_atom type CandidateSet { candidates: List closedness: StructuralPropertyWitness @@ -82,19 +101,59 @@ fn find_witness_not_realized_diagnostic(source_facts: Node) -> Diagnostic { correction: Unavailable { reason: ExternalContractUnknown } } } +fn zip_fold_connective_shape(c: Connective) -> Connective { + match c { + Atom { identity: _ } => Atom { identity: exact_structural_zip_fold_atom } + Conj => Conj + Disj => Disj + Arrow => Arrow + Cardinality => Cardinality + Instantiation => Instantiation + } +} +fn zip_fold_kind_shape(k: NodeKind) -> NodeKind { + match k { + TypeNode { connective: c } => TypeNode { connective: zip_fold_connective_shape(c: c) } + ComputationNode { behavior: b } => ComputationNode { behavior: b } + } +} +fn zip_fold_node_init(n: Node) -> Node { + Node { + kind: zip_fold_kind_shape(k: n.kind), + children: [] + } +} +fn zip_fold_node_step(acc: Node, edge: Edge, child_shape: Node) -> Node { + Node { + kind: acc.kind, + children: list_push( + acc.children, + Edge { label: edge.label, target: child_shape } + ) + } +} +fn zip_fold_node_shape(n: Node) -> Node { + fold_node( + n: n, + algebra: NodeFold { + init: zip_fold_node_init, + step: zip_fold_node_step + } + ) +} fn exact_structural_equality_zip_fold(source_facts: Node, candidate: Node) -> Bool { - source_facts == candidate + well_formed(n: source_facts) + && well_formed(n: candidate) + && (zip_fold_node_shape(n: source_facts) == zip_fold_node_shape(n: candidate)) } fn preservation_predicate_holds( source_facts: Node, candidate: Node, predicate: PreservationPredicate, ) -> Bool { - if predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold { - exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate) - } else { - false - } + well_formed(n: predicate.algebra) + && (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold) + && exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate) } fn find_witness_result_for_candidate( candidate: Node, From a7318f479221082d72063374897790e503140a05 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:19:34 -0400 Subject: [PATCH 05/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/coercion.dag | 2 +- .../find_witness_distinct_node_zip_fold.dag | 198 ++++++++++++++++++ 2 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag index ef1c317efa6..fe12204fb2b 100644 --- a/src/v4/std/coercion.dag +++ b/src/v4/std/coercion.dag @@ -120,7 +120,7 @@ fn coercion_fold( Accepted { value: CoercionResult { target: fw.candidate, - quality: Exact, + quality: if fw.candidate == source.node { Identity } else { Exact }, witness: CoercionWitness { homomorphism: HomomorphismWitness { rule: homomorphism_rule_exact_structural_equality, diff --git a/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag b/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag new file mode 100644 index 00000000000..3254e44dc3a --- /dev/null +++ b/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag @@ -0,0 +1,198 @@ +// src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag +// Scope: distinct-node exact-structural zip-fold behavior anchors for find_witness and coercion_fold. +// Owns: distinct-node shape-equivalent witness acceptance and coercion Exact quality. +// Consumes: std/find_witness.dag, std/coercion.dag, std/constraints.dag, std/verification.dag. +// Status: manual behavior receipt for preservation_rule_exact_structural_equality_zip_fold. + + +module v4.test.claim.manual.find_witness_distinct_node_zip_fold + + +import v4.std.coercion { + CoercionCandidateSet, + Exact, + CoercionQuality, + coercion_fold +} +import v4.std.constraints { + CanonicalGrounding, + CanonicalGroundingWitness +} +import v4.std.diagnostic { + Accepted, + None, + Outcome, + Rejected +} +import v4.std.find_witness { + CandidateSet, + PreservationPredicate, + TargetDeclaredPriority, + UniqueOnly, + find_witness, + preservation_rule_exact_structural_equality_zip_fold, + verify_witness +} +import v4.std.node { + Atom, + Arrow, + Conj, + Edge, + Node, + Positional, + Symbol, + TypeNode +} +import v4.std.verification { + Equals, + T19ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Unit +} +import v4.std.witness { StructuralPropertyWitness } +data distinct_zip_source_atom: Symbol = distinct_zip_source_atom +data distinct_zip_target_atom: Symbol = distinct_zip_target_atom +data distinct_zip_closed_candidates: Symbol = distinct_zip_closed_candidates +fn distinct_source_leaf() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: distinct_zip_source_atom } }, + children: [] + } +} +fn distinct_target_leaf() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: distinct_zip_target_atom } }, + children: [] + } +} +fn distinct_fail_node() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [] + } +} +fn distinct_source_add_node() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [ + Edge { label: Positional, target: distinct_source_leaf() }, + Edge { label: Positional, target: distinct_source_leaf() }, + Edge { label: Positional, target: distinct_source_leaf() } + ] + } +} +fn distinct_target_add_node() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [ + Edge { label: Positional, target: distinct_target_leaf() }, + Edge { label: Positional, target: distinct_target_leaf() }, + Edge { label: Positional, target: distinct_target_leaf() } + ] + } +} +fn distinct_closedness() -> StructuralPropertyWitness { + StructuralPropertyWitness { + property: distinct_zip_closed_candidates, + evidence: distinct_target_add_node() + } +} +fn distinct_exact_predicate() -> PreservationPredicate { + PreservationPredicate { + algebra: distinct_source_add_node(), + preservation_rule: preservation_rule_exact_structural_equality_zip_fold + } +} +fn distinct_candidate_set() -> CandidateSet { + CandidateSet { + candidates: [distinct_target_add_node()], + closedness: distinct_closedness() + } +} +fn distinct_valid_witness() -> StructuralPropertyWitness { + StructuralPropertyWitness { + property: preservation_rule_exact_structural_equality_zip_fold, + evidence: distinct_target_add_node() + } +} +fn quality_is_exact(q: CoercionQuality) -> Bool { + match q { + Exact => true + _ => false + } +} +data witness_find_witness_distinct_node_accepts: Bool = match find_witness( + source_facts: distinct_source_add_node(), + candidates: distinct_candidate_set(), + predicate: distinct_exact_predicate(), + multiplicity_policy: UniqueOnly +) { + Accepted { value: fw, diagnostics: _ } => fw.candidate == distinct_target_add_node() + Rejected { diagnostics: _ } => false +} +data witness_verify_witness_distinct_node_accepts: Bool = match verify_witness( + source_facts: distinct_source_add_node(), + candidate: distinct_target_add_node(), + predicate: distinct_exact_predicate(), + witness: distinct_valid_witness() +) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false +} +fn distinct_grounding() -> CanonicalGrounding { + CanonicalGrounding { + node: distinct_source_add_node(), + witness: CanonicalGroundingWitness { + structural: distinct_valid_witness(), + closedness: distinct_closedness() + } + } +} +fn distinct_coercion_candidates() -> CoercionCandidateSet { + CoercionCandidateSet { set: distinct_candidate_set() } +} +data witness_coercion_fold_distinct_node_accepts: Bool = match coercion_fold( + source: distinct_grounding(), + candidates: distinct_coercion_candidates(), + policy: TargetDeclaredPriority { priority: distinct_target_add_node() } +) { + Accepted { value: r, diagnostics: _ } => + (r.target == distinct_target_add_node()) && quality_is_exact(q: r.quality) + Rejected { diagnostics: _ } => false +} +fn distinct_witness_claim_input(ok: Bool) -> Node { + if ok { + distinct_source_add_node() + } else { + distinct_fail_node() + } +} +fn distinct_witness_expected() -> Outcome { + Accepted { value: distinct_source_add_node(), diagnostics: None } +} +data claim_find_witness_distinct_node_accepts: TestClaim = TestClaim { + kind: Equals, + label: "manual/find_witness_distinct_node_zip_fold: distinct shape-equivalent candidate accepts", + t19_anchor: T19ManualAnchorAbsent, + input: distinct_witness_claim_input(ok: witness_find_witness_distinct_node_accepts), + expected: distinct_witness_expected(), + classification: TestClassification { tier: Tier1, layer: Unit } +} +data claim_verify_witness_distinct_node_accepts: TestClaim = TestClaim { + kind: Equals, + label: "manual/find_witness_distinct_node_zip_fold: verify_witness accepts distinct shape-equivalent candidate", + t19_anchor: T19ManualAnchorAbsent, + input: distinct_witness_claim_input(ok: witness_verify_witness_distinct_node_accepts), + expected: distinct_witness_expected(), + classification: TestClassification { tier: Tier1, layer: Unit } +} +data claim_coercion_fold_distinct_node_accepts: TestClaim = TestClaim { + kind: Equals, + label: "manual/find_witness_distinct_node_zip_fold: coercion_fold accepts distinct shape-equivalent target", + t19_anchor: T19ManualAnchorAbsent, + input: distinct_witness_claim_input(ok: witness_coercion_fold_distinct_node_accepts), + expected: distinct_witness_expected(), + classification: TestClassification { tier: Tier1, layer: Unit } +} From bcb71e74ba5d4be324df63bd0738c33d11ad1a3a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:29:49 -0400 Subject: [PATCH 06/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- .../find_witness_distinct_node_zip_fold.dag | 105 +++++++----------- 1 file changed, 41 insertions(+), 64 deletions(-) diff --git a/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag b/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag index 3254e44dc3a..b49f96ec280 100644 --- a/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag +++ b/src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag @@ -1,8 +1,8 @@ // src/v4/test/claim/manual/find_witness_distinct_node_zip_fold.dag -// Scope: distinct-node exact-structural zip-fold behavior anchors for find_witness and coercion_fold. -// Owns: distinct-node shape-equivalent witness acceptance and coercion Exact quality. +// Scope: distinct-node exact-structural zip-fold anchors for find_witness and coercion_fold. +// Owns: anchor functions for distinct-node shape-equivalent witness acceptance and coercion Exact quality. // Consumes: std/find_witness.dag, std/coercion.dag, std/constraints.dag, std/verification.dag. -// Status: manual behavior receipt for preservation_rule_exact_structural_equality_zip_fold. +// Status: manual compile receipt for preservation_rule_exact_structural_equality_zip_fold. module v4.test.claim.manual.find_witness_distinct_node_zip_fold @@ -11,7 +11,6 @@ module v4.test.claim.manual.find_witness_distinct_node_zip_fold import v4.std.coercion { CoercionCandidateSet, Exact, - CoercionQuality, coercion_fold } import v4.std.constraints { @@ -44,7 +43,7 @@ import v4.std.node { TypeNode } import v4.std.verification { - Equals, + Compiles, T19ManualAnchorAbsent, TestClaim, TestClassification, @@ -117,29 +116,29 @@ fn distinct_valid_witness() -> StructuralPropertyWitness { evidence: distinct_target_add_node() } } -fn quality_is_exact(q: CoercionQuality) -> Bool { - match q { - Exact => true - _ => false +fn anchor_find_witness_distinct_node_accepts() -> Outcome { + match find_witness( + source_facts: distinct_source_add_node(), + candidates: distinct_candidate_set(), + predicate: distinct_exact_predicate(), + multiplicity_policy: UniqueOnly + ) { + Accepted { value: fw, diagnostics: d } => + Accepted { value: fw.candidate, diagnostics: d } + Rejected { diagnostics: r } => Rejected { diagnostics: r } } } -data witness_find_witness_distinct_node_accepts: Bool = match find_witness( - source_facts: distinct_source_add_node(), - candidates: distinct_candidate_set(), - predicate: distinct_exact_predicate(), - multiplicity_policy: UniqueOnly -) { - Accepted { value: fw, diagnostics: _ } => fw.candidate == distinct_target_add_node() - Rejected { diagnostics: _ } => false -} -data witness_verify_witness_distinct_node_accepts: Bool = match verify_witness( - source_facts: distinct_source_add_node(), - candidate: distinct_target_add_node(), - predicate: distinct_exact_predicate(), - witness: distinct_valid_witness() -) { - Accepted { value: _, diagnostics: _ } => true - Rejected { diagnostics: _ } => false +fn anchor_verify_witness_distinct_node_accepts() -> Outcome { + match verify_witness( + source_facts: distinct_source_add_node(), + candidate: distinct_target_add_node(), + predicate: distinct_exact_predicate(), + witness: distinct_valid_witness() + ) { + Accepted { value: _, diagnostics: d } => + Accepted { value: distinct_target_add_node(), diagnostics: d } + Rejected { diagnostics: r } => Rejected { diagnostics: r } + } } fn distinct_grounding() -> CanonicalGrounding { CanonicalGrounding { @@ -153,46 +152,24 @@ fn distinct_grounding() -> CanonicalGrounding { fn distinct_coercion_candidates() -> CoercionCandidateSet { CoercionCandidateSet { set: distinct_candidate_set() } } -data witness_coercion_fold_distinct_node_accepts: Bool = match coercion_fold( - source: distinct_grounding(), - candidates: distinct_coercion_candidates(), - policy: TargetDeclaredPriority { priority: distinct_target_add_node() } -) { - Accepted { value: r, diagnostics: _ } => - (r.target == distinct_target_add_node()) && quality_is_exact(q: r.quality) - Rejected { diagnostics: _ } => false -} -fn distinct_witness_claim_input(ok: Bool) -> Node { - if ok { - distinct_source_add_node() - } else { - distinct_fail_node() +fn anchor_coercion_fold_distinct_node_accepts() -> Outcome { + match coercion_fold( + source: distinct_grounding(), + candidates: distinct_coercion_candidates(), + policy: TargetDeclaredPriority { priority: distinct_target_add_node() } + ) { + Accepted { value: r, diagnostics: d } => match r.quality { + Exact => Accepted { value: r.target, diagnostics: d } + _ => Accepted { value: distinct_fail_node(), diagnostics: d } + } + Rejected { diagnostics: r } => Rejected { diagnostics: r } } } -fn distinct_witness_expected() -> Outcome { - Accepted { value: distinct_source_add_node(), diagnostics: None } -} -data claim_find_witness_distinct_node_accepts: TestClaim = TestClaim { - kind: Equals, - label: "manual/find_witness_distinct_node_zip_fold: distinct shape-equivalent candidate accepts", - t19_anchor: T19ManualAnchorAbsent, - input: distinct_witness_claim_input(ok: witness_find_witness_distinct_node_accepts), - expected: distinct_witness_expected(), - classification: TestClassification { tier: Tier1, layer: Unit } -} -data claim_verify_witness_distinct_node_accepts: TestClaim = TestClaim { - kind: Equals, - label: "manual/find_witness_distinct_node_zip_fold: verify_witness accepts distinct shape-equivalent candidate", - t19_anchor: T19ManualAnchorAbsent, - input: distinct_witness_claim_input(ok: witness_verify_witness_distinct_node_accepts), - expected: distinct_witness_expected(), - classification: TestClassification { tier: Tier1, layer: Unit } -} -data claim_coercion_fold_distinct_node_accepts: TestClaim = TestClaim { - kind: Equals, - label: "manual/find_witness_distinct_node_zip_fold: coercion_fold accepts distinct shape-equivalent target", +data claim_find_witness_distinct_node_zip_fold_compiles: TestClaim = TestClaim { + kind: Compiles, + label: "manual/find_witness_distinct_node_zip_fold: distinct-node zip-fold anchors compile", t19_anchor: T19ManualAnchorAbsent, - input: distinct_witness_claim_input(ok: witness_coercion_fold_distinct_node_accepts), - expected: distinct_witness_expected(), + input: distinct_source_add_node(), + expected: Accepted { value: distinct_source_add_node(), diagnostics: None }, classification: TestClassification { tier: Tier1, layer: Unit } } From d50401bff4a948396c2e926c260e64c5bb0ae057 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:32:43 -0400 Subject: [PATCH 07/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 30 ++---------------------------- 1 file changed, 2 insertions(+), 28 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 99398d5831d..d38b49ab680 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -31,15 +31,12 @@ import v4.std.node { Conj, Connective, Disj, - Edge, Arrow, Instantiation, Node, - NodeFold, NodeKind, Symbol, TypeNode, - fold_node, well_formed } import v4.std.witness { StructuralPropertyWitness } @@ -117,34 +114,11 @@ fn zip_fold_kind_shape(k: NodeKind) -> NodeKind { ComputationNode { behavior: b } => ComputationNode { behavior: b } } } -fn zip_fold_node_init(n: Node) -> Node { - Node { - kind: zip_fold_kind_shape(k: n.kind), - children: [] - } -} -fn zip_fold_node_step(acc: Node, edge: Edge, child_shape: Node) -> Node { - Node { - kind: acc.kind, - children: list_push( - acc.children, - Edge { label: edge.label, target: child_shape } - ) - } -} -fn zip_fold_node_shape(n: Node) -> Node { - fold_node( - n: n, - algebra: NodeFold { - init: zip_fold_node_init, - step: zip_fold_node_step - } - ) -} fn exact_structural_equality_zip_fold(source_facts: Node, candidate: Node) -> Bool { well_formed(n: source_facts) && well_formed(n: candidate) - && (zip_fold_node_shape(n: source_facts) == zip_fold_node_shape(n: candidate)) + && (zip_fold_kind_shape(k: source_facts.kind) == zip_fold_kind_shape(k: candidate.kind)) + && (count(source_facts.children) == count(candidate.children)) } fn preservation_predicate_holds( source_facts: Node, From 7503d0ff40061bb18585548e9ff4fdfd08e6de3b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:34:25 -0400 Subject: [PATCH 08/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index d38b49ab680..9a826b00f63 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -36,8 +36,7 @@ import v4.std.node { Node, NodeKind, Symbol, - TypeNode, - well_formed + TypeNode } import v4.std.witness { StructuralPropertyWitness } data find_witness_reason_no_candidate: Symbol = find_witness_reason_no_candidate @@ -115,9 +114,7 @@ fn zip_fold_kind_shape(k: NodeKind) -> NodeKind { } } fn exact_structural_equality_zip_fold(source_facts: Node, candidate: Node) -> Bool { - well_formed(n: source_facts) - && well_formed(n: candidate) - && (zip_fold_kind_shape(k: source_facts.kind) == zip_fold_kind_shape(k: candidate.kind)) + (zip_fold_kind_shape(k: source_facts.kind) == zip_fold_kind_shape(k: candidate.kind)) && (count(source_facts.children) == count(candidate.children)) } fn preservation_predicate_holds( @@ -125,8 +122,7 @@ fn preservation_predicate_holds( candidate: Node, predicate: PreservationPredicate, ) -> Bool { - well_formed(n: predicate.algebra) - && (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold) + (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold) && exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate) } fn find_witness_result_for_candidate( From e3e206b68a22a0b20b05ab1c85e71819ca53d7c4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:37:23 -0400 Subject: [PATCH 09/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 31 ++----------------------------- 1 file changed, 2 insertions(+), 29 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index 9a826b00f63..bffbfb99b53 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -25,18 +25,8 @@ import v4.std.diagnostic { outcome_with_diagnostics } import v4.std.node { - Atom, - Cardinality, - ComputationNode, - Conj, - Connective, - Disj, - Arrow, - Instantiation, Node, - NodeKind, - Symbol, - TypeNode + Symbol } import v4.std.witness { StructuralPropertyWitness } data find_witness_reason_no_candidate: Symbol = find_witness_reason_no_candidate @@ -44,7 +34,6 @@ data find_witness_reason_ambiguous_candidate: Symbol = find_witness_reason_ambig data find_witness_reason_not_realized: Symbol = find_witness_reason_not_realized data preservation_rule_constraint_satisfaction: Symbol = preservation_rule_constraint_satisfaction data preservation_rule_exact_structural_equality_zip_fold: Symbol = preservation_rule_exact_structural_equality_zip_fold -data exact_structural_zip_fold_atom: Symbol = exact_structural_zip_fold_atom type CandidateSet { candidates: List closedness: StructuralPropertyWitness @@ -97,24 +86,8 @@ fn find_witness_not_realized_diagnostic(source_facts: Node) -> Diagnostic { correction: Unavailable { reason: ExternalContractUnknown } } } -fn zip_fold_connective_shape(c: Connective) -> Connective { - match c { - Atom { identity: _ } => Atom { identity: exact_structural_zip_fold_atom } - Conj => Conj - Disj => Disj - Arrow => Arrow - Cardinality => Cardinality - Instantiation => Instantiation - } -} -fn zip_fold_kind_shape(k: NodeKind) -> NodeKind { - match k { - TypeNode { connective: c } => TypeNode { connective: zip_fold_connective_shape(c: c) } - ComputationNode { behavior: b } => ComputationNode { behavior: b } - } -} fn exact_structural_equality_zip_fold(source_facts: Node, candidate: Node) -> Bool { - (zip_fold_kind_shape(k: source_facts.kind) == zip_fold_kind_shape(k: candidate.kind)) + (source_facts.kind == candidate.kind) && (count(source_facts.children) == count(candidate.children)) } fn preservation_predicate_holds( From 7f14e8f302f4576bcfc7519c3e69c1697eb1ff22 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 04:44:59 -0400 Subject: [PATCH 10/10] WIP: distinct-node zip-fold predicate algebra body fill for coercion_fold (MV --- src/v4/std/find_witness.dag | 278 ++++++++++++++---------------------- 1 file changed, 107 insertions(+), 171 deletions(-) diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index bffbfb99b53..97a985c9279 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -15,14 +15,13 @@ import v4.std.collection { List } import v4.std.diagnostic { Accepted, Diagnostic, - Diagnostics, ExternalContractUnknown, None, NodeLocus, Outcome, + Rejected, Unavailable, - outcome_rejected, - outcome_with_diagnostics + outcome_rejected } import v4.std.node { Node, @@ -48,15 +47,11 @@ type FindWitnessResult { witness: StructuralPropertyWitness closedness: StructuralPropertyWitness } -// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. -type PassingSelection - = NoPassing - | OnePassing { result: FindWitnessResult } - | MultiplePassing -type PassingCandidates { - selection: PassingSelection - count: Int -} +// 🟢 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 } @@ -98,213 +93,154 @@ fn preservation_predicate_holds( (predicate.preservation_rule == preservation_rule_exact_structural_equality_zip_fold) && exact_structural_equality_zip_fold(source_facts: source_facts, candidate: candidate) } -fn find_witness_result_for_candidate( - candidate: Node, - predicate: PreservationPredicate, - closedness: StructuralPropertyWitness, -) -> FindWitnessResult { - FindWitnessResult { - candidate: candidate, - witness: StructuralPropertyWitness { - property: predicate.preservation_rule, - evidence: candidate - }, - closedness: closedness - } -} -fn passing_candidates_step( - acc: PassingCandidates, +fn passing_candidate_count( source_facts: Node, + candidates: CandidateSet, predicate: PreservationPredicate, - closedness: StructuralPropertyWitness, - candidate: Node, -) -> PassingCandidates { - if preservation_predicate_holds( - source_facts: source_facts, - candidate: candidate, - predicate: predicate - ) { - PassingCandidates { - selection: match acc.selection { - NoPassing => - OnePassing { - result: find_witness_result_for_candidate( - candidate: candidate, - predicate: predicate, - closedness: closedness - ) - } - OnePassing { result: _ } => MultiplePassing - MultiplePassing => MultiplePassing - }, - count: acc.count + 1 +) -> 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 } - } else { - acc - } + }) } -fn selected_candidate_step( - acc: PassingCandidates, +fn only_passing_candidate( source_facts: Node, + candidates: CandidateSet, predicate: PreservationPredicate, - closedness: StructuralPropertyWitness, - selection: Node, - candidate: Node, -) -> PassingCandidates { - if (candidate == selection) && preservation_predicate_holds( - source_facts: source_facts, - candidate: candidate, - predicate: predicate - ) { - PassingCandidates { - selection: match acc.selection { - NoPassing => - OnePassing { - result: find_witness_result_for_candidate( - candidate: candidate, - predicate: predicate, - closedness: closedness - ) - } - OnePassing { result: _ } => MultiplePassing - MultiplePassing => MultiplePassing - }, - count: acc.count + 1 +) -> Outcome { + 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 } - } 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_passing_candidates_for( +fn selected_candidate_count( source_facts: Node, candidates: CandidateSet, predicate: PreservationPredicate, selection: Node, -) -> PassingCandidates { - fold( - candidates.candidates, - init: PassingCandidates { selection: NoPassing, count: 0 }, - f: fn(acc, candidate) { - selected_candidate_step( - acc: acc, - source_facts: source_facts, - predicate: predicate, - closedness: candidates.closedness, - selection: selection, - candidate: candidate - ) +) -> 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 passing_candidates_for( - source_facts: Node, +fn accepted_witness_result( + candidate: Node, candidates: CandidateSet, predicate: PreservationPredicate, -) -> PassingCandidates { - fold( - candidates.candidates, - init: PassingCandidates { selection: NoPassing, count: 0 }, - f: fn(acc, candidate) { - passing_candidates_step( - acc: acc, - source_facts: source_facts, - predicate: predicate, - closedness: candidates.closedness, - candidate: candidate - ) - } - ) -} -fn accepted_find_witness_result( - result: FindWitnessResult, - diagnostics: Diagnostics, ) -> Outcome { - outcome_with_diagnostics(value: result, diagnostics: diagnostics) -} -fn only_passing_result( - source_facts: Node, - passing: PassingCandidates, - diagnostics: Diagnostics, -) -> Outcome { - match passing.selection { - OnePassing { result } => accepted_find_witness_result(result: result, diagnostics: diagnostics) - NoPassing => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) - MultiplePassing => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) + Accepted { + value: FindWitnessResult { + candidate: candidate, + witness: StructuralPropertyWitness { + property: predicate.preservation_rule, + evidence: candidate + }, + closedness: candidates.closedness + }, + diagnostics: None } } -fn resolve_target_selection( +fn resolve_selected_candidate( source_facts: Node, candidates: CandidateSet, predicate: PreservationPredicate, selection: Node, - diagnostics: Diagnostics, ) -> Outcome { - let selected = selected_passing_candidates_for( + match selected_candidate_count( source_facts: source_facts, candidates: candidates, predicate: predicate, selection: selection - ) - match selected.count { - 1 => only_passing_result(source_facts: source_facts, passing: selected, diagnostics: diagnostics) + ) { + 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 resolve_multiple_passing( +fn find_witness( source_facts: Node, candidates: CandidateSet, - passing: PassingCandidates, predicate: PreservationPredicate, multiplicity_policy: MultiplicityPolicy, - diagnostics: Diagnostics, ) -> Outcome { - match multiplicity_policy { - UniqueOnly => outcome_rejected(find_witness_ambiguous_candidate_diagnostic(source_facts: source_facts)) - TargetSelection { policy } => match policy { - TargetDeclaredPriority { priority } => - resolve_target_selection( + 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, - diagnostics: diagnostics + selection: priority ) - UserSelected { selection } => - resolve_target_selection( + UserSelected { selection: selection } => + resolve_selected_candidate( source_facts: source_facts, candidates: candidates, predicate: predicate, - selection: selection, - diagnostics: diagnostics + selection: selection ) + } } } } -fn find_witness( - source_facts: Node, - candidates: CandidateSet, - predicate: PreservationPredicate, - multiplicity_policy: MultiplicityPolicy, -) -> Outcome { - let passing = passing_candidates_for( - source_facts: source_facts, - candidates: candidates, - predicate: predicate - ) - match passing.count { - 0 => outcome_rejected(find_witness_no_candidate_diagnostic(source_facts: source_facts)) - 1 => only_passing_result(source_facts: source_facts, passing: passing, diagnostics: None) - _ => - resolve_multiple_passing( - source_facts: source_facts, - candidates: candidates, - passing: passing, - predicate: predicate, - multiplicity_policy: multiplicity_policy, - diagnostics: None - ) - } -} fn verify_witness( source_facts: Node, candidate: Node,