From 4d7dba12da37ed25844ee8b88071c898ac5fc346 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 3 Jun 2026 02:20:15 +0000 Subject: [PATCH 1/2] WIP: W3.2 coercion realization (Rung 3): preservation_rule_refinement_widenin --- src/v4/extdeps/coercion_widening.dag | 50 ++++++++++++ src/v4/std/coercion.dag | 5 +- src/v4/std/find_witness.dag | 25 +++++- src/v4/std/refinement_widening_predicate.dag | 81 ++++++++++++++++++++ 4 files changed, 159 insertions(+), 2 deletions(-) create mode 100644 src/v4/extdeps/coercion_widening.dag create mode 100644 src/v4/std/refinement_widening_predicate.dag diff --git a/src/v4/extdeps/coercion_widening.dag b/src/v4/extdeps/coercion_widening.dag new file mode 100644 index 00000000000..929da1465e5 --- /dev/null +++ b/src/v4/extdeps/coercion_widening.dag @@ -0,0 +1,50 @@ +// src/v4/extdeps/coercion_widening.dag +// Scope: cross-target faithful refinement widening pair registry (MVP rust i32 → python int). +// Anchor: ROADMAP.md coercion (i32 → arbitrary-precision int); W3.2 Leg B. +// Status: MVP pair table lives here; std/refinement_widening_predicate proves bundle evidence (P2). + + +module v4.extdeps.coercion_widening + + +import v4.extdeps.languages.python { python_int_inhabitant_node } +import v4.extdeps.languages.rust { rust_inhabitant_i32_node } +import v4.std.coercion { + CoercionCandidateSet, + CoercionResult, + coercion_fold_refinement_widening +} +import v4.std.constraints { CanonicalGrounding } +import v4.std.diagnostic { Outcome } +import v4.std.find_witness { + PreservationPredicate, + TargetDeclaredPriority, + preservation_rule_refinement_widening +} +import v4.std.node { Node } +import v4.std.refinement_widening_predicate { refinement_widening_predicate_algebra } + + +fn mvp_rust_i32_python_int_refinement_widening_predicate() -> PreservationPredicate { + PreservationPredicate { + algebra: refinement_widening_predicate_algebra( + source: rust_inhabitant_i32_node(), + candidate: python_int_inhabitant_node() + ), + preservation_rule: preservation_rule_refinement_widening + } +} + + +fn coercion_fold_mvp_rust_i32_to_python_int_widening( + source: CanonicalGrounding, + candidates: CoercionCandidateSet, + priority: Node, +) -> Outcome { + coercion_fold_refinement_widening( + source: source, + candidates: candidates, + policy: TargetDeclaredPriority { priority: priority }, + predicate: mvp_rust_i32_python_int_refinement_widening_predicate() + ) +} diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag index 7aa3327bfa8..a400541bcdb 100644 --- a/src/v4/std/coercion.dag +++ b/src/v4/std/coercion.dag @@ -36,7 +36,8 @@ import v4.std.find_witness { find_witness_reason_invalid_witness, find_witness_reason_no_candidate, find_witness_reason_not_realized, - preservation_rule_exact_structural_equality_zip_fold + preservation_rule_exact_structural_equality_zip_fold, + preservation_rule_refinement_widening } import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed } import v4.std.witness { HomomorphismWitness, StructuralPropertyWitness } @@ -46,6 +47,7 @@ data coercion_homomorphism_evidence_source: Symbol = coercion_homomorphism_evide 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 homomorphism_rule_refinement_widening: Symbol = homomorphism_rule_refinement_widening 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 @@ -63,6 +65,7 @@ type FindWitnessRejectionKind type CoercionQuality = Identity | Exact + | Widened // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. type CoercionMismatchKind = NoTargetCandidate diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index cf581b40f7c..bbf6e8ac993 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -25,6 +25,7 @@ import v4.std.constraint_satisfaction_predicate { import v4.std.exact_structural_equality_zip_fold_predicate { exact_structural_equality_zip_fold_preservation_holds } +import v4.std.refinement_widening_predicate { refinement_widening_preservation_holds } 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 @@ -33,6 +34,7 @@ data find_witness_reason_not_realized: Symbol = find_witness_reason_not_realized data find_witness_reason_invalid_witness: Symbol = find_witness_reason_invalid_witness 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 preservation_rule_refinement_widening: Symbol = preservation_rule_refinement_widening type CandidateSet { candidates: List closedness: StructuralPropertyWitness @@ -114,6 +116,12 @@ fn preservation_predicate_holds( candidate: candidate, algebra: predicate.algebra ) + preservation_rule_refinement_widening => + refinement_widening_preservation_holds( + source_facts: source_facts, + candidate: candidate, + algebra: predicate.algebra + ) _ => false } } @@ -240,6 +248,13 @@ fn find_witness( predicate: predicate, multiplicity_policy: multiplicity_policy ) + preservation_rule_refinement_widening => + find_witness_realized( + source_facts: source_facts, + candidates: candidates, + predicate: predicate, + multiplicity_policy: multiplicity_policy + ) _ => outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts)) } } @@ -250,7 +265,8 @@ fn find_witness_realized( multiplicity_policy: MultiplicityPolicy ) -> Outcome { if (predicate.preservation_rule != preservation_rule_constraint_satisfaction) - && (predicate.preservation_rule != preservation_rule_exact_structural_equality_zip_fold) { + && (predicate.preservation_rule != preservation_rule_exact_structural_equality_zip_fold) + && (predicate.preservation_rule != preservation_rule_refinement_widening) { outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts)) } else { let passing_count = passing_candidate_count( @@ -316,6 +332,13 @@ fn verify_witness( predicate: predicate, witness: witness ) + preservation_rule_refinement_widening => + verify_witness_realized( + source_facts: source_facts, + candidate: candidate, + predicate: predicate, + witness: witness + ) _ => outcome_rejected(find_witness_not_realized_diagnostic(source_facts: source_facts)) } } diff --git a/src/v4/std/refinement_widening_predicate.dag b/src/v4/std/refinement_widening_predicate.dag new file mode 100644 index 00000000000..b78b624af2a --- /dev/null +++ b/src/v4/std/refinement_widening_predicate.dag @@ -0,0 +1,81 @@ +// src/v4/std/refinement_widening_predicate.dag +// Scope: mechanical refinement-widening preservation check (leaf — no extdeps import). +// Anchor: ROADMAP.md coercion faithful widening; design-v4-compiler-homomorphism.md Pass B. +// Status: bundle-encoded pair evidence on PreservationPredicate.algebra; axis-general registry is forward work. + + +module v4.std.refinement_widening_predicate + + +import v4.std.diagnostic { Accepted, Outcome, Rejected } +import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed } +import v4.std.node_query { find_named_child } + + +data refinement_widening_field_source: Symbol = refinement_widening_field_source +data refinement_widening_field_candidate: Symbol = refinement_widening_field_candidate +data refinement_widening_field_source_facts: Symbol = refinement_widening_field_source_facts + + +fn refinement_widening_predicate_algebra( + source: Node, + candidate: Node, +) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: refinement_widening_field_source }, + target: source + }, + Edge { + label: Named { name: refinement_widening_field_candidate }, + target: candidate + }, + Edge { + label: Named { name: refinement_widening_field_source_facts }, + target: source + } + ] + } +} + + +fn refinement_widening_bundle_holds( + source_facts: Node, + candidate: Node, + algebra: Node, +) -> Bool { + match find_named_child(root: algebra, name: refinement_widening_field_source) { + Accepted { value: bundled_source, diagnostics: None } => + match find_named_child(root: algebra, name: refinement_widening_field_candidate) { + Accepted { value: bundled_candidate, diagnostics: None } => + match find_named_child(root: algebra, name: refinement_widening_field_source_facts) { + Accepted { value: bundled_source_facts, diagnostics: None } => + (bundled_source == source_facts) + && (bundled_candidate == candidate) + && (bundled_source_facts == source_facts) + && (source_facts != candidate) + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + + +fn refinement_widening_preservation_holds( + source_facts: Node, + candidate: Node, + algebra: Node, +) -> Bool { + well_formed(n: source_facts) + && well_formed(n: algebra) + && well_formed(n: candidate) + && refinement_widening_bundle_holds( + source_facts: source_facts, + candidate: candidate, + algebra: algebra + ) +} From 0dd85d07a45f1074410e6c12c03a3de39ec1bcfd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 3 Jun 2026 02:23:33 +0000 Subject: [PATCH 2/2] =?UTF-8?q?feat(v4):=20W3.2=20Leg=20B=20=E2=80=94=20co?= =?UTF-8?q?ercion=5Ffold=5Frefinement=5Fwidening=20+=20rust=20i32=E2=86=92?= =?UTF-8?q?python=20int=20Accepted?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wire CoercionQuality::Widened and homomorphism_rule_refinement_widening through coercion_fold_refinement_widening; complete find_witness dispatch for the widening predicate. Add Leg B TestClaim receipt (mvp_int_cross_target) and Widened match arms on existing coercion quality helpers. Co-authored-by: Cursor --- src/v4/std/coercion.dag | 60 ++++++++++++- .../find_witness_distinct_node_zip_fold.dag | 1 + .../manual/find_witness_identity_mvp.dag | 1 + .../manual/mvp_int_cross_target_coercion.dag | 86 ++++++++++++++++++- 4 files changed, 144 insertions(+), 4 deletions(-) diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag index a400541bcdb..17895fb2aca 100644 --- a/src/v4/std/coercion.dag +++ b/src/v4/std/coercion.dag @@ -247,7 +247,7 @@ fn coercion_homomorphism_evidence( ] } } -fn coercion_fold( +fn coercion_fold_exact_structural( source: CanonicalGrounding, candidates: CoercionCandidateSet, policy: TargetSelectionPolicy, @@ -283,6 +283,51 @@ fn coercion_fold( } } } +fn coercion_fold( + source: CanonicalGrounding, + candidates: CoercionCandidateSet, + policy: TargetSelectionPolicy, +) -> Outcome { + coercion_fold_exact_structural( + source: source, + candidates: candidates, + policy: policy + ) +} +fn coercion_fold_refinement_widening( + source: CanonicalGrounding, + candidates: CoercionCandidateSet, + policy: TargetSelectionPolicy, + predicate: PreservationPredicate, +) -> Outcome { + match find_witness( + source_facts: source.node, + candidates: candidates.set, + predicate: predicate, + multiplicity_policy: TargetSelection { policy: policy } + ) { + Accepted { value: fw, diagnostics: fw_d } => + Accepted { + value: CoercionResult { + target: fw.candidate, + quality: Widened, + witness: CoercionWitness { + homomorphism: HomomorphismWitness { + rule: homomorphism_rule_refinement_widening, + evidence: coercion_homomorphism_evidence(source: source, fw: fw) + } + } + }, + diagnostics: fw_d + } + Rejected { diagnostics: r } => + match coercion_wrap_find_witness_rejection(source: source, upstream: r) { + Accepted { value: wrapped, diagnostics: _ } => + Rejected { diagnostics: wrapped } + Rejected { diagnostics: wrap_r } => Rejected { diagnostics: wrap_r } + } + } +} fn coercion_fold_with_declared_priority( source: CanonicalGrounding, candidates: CoercionCandidateSet, @@ -294,3 +339,16 @@ fn coercion_fold_with_declared_priority( policy: TargetDeclaredPriority { priority: priority } ) } +fn coercion_fold_refinement_widening_with_declared_priority( + source: CanonicalGrounding, + candidates: CoercionCandidateSet, + priority: Node, + predicate: PreservationPredicate, +) -> Outcome { + coercion_fold_refinement_widening( + source: source, + candidates: candidates, + policy: TargetDeclaredPriority { priority: priority }, + predicate: predicate + ) +} 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 8bc62d84c47..e935f599a91 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 @@ -195,6 +195,7 @@ fn quality_is_exact(q: CoercionQuality) -> Bool { match q { Exact => true Identity => false + Widened => false } } data witness_find_witness_distinct_node_accepts: Bool = match find_witness( diff --git a/src/v4/test/claim/manual/find_witness_identity_mvp.dag b/src/v4/test/claim/manual/find_witness_identity_mvp.dag index 0c2e0ab36f5..d039584b273 100644 --- a/src/v4/test/claim/manual/find_witness_identity_mvp.dag +++ b/src/v4/test/claim/manual/find_witness_identity_mvp.dag @@ -153,6 +153,7 @@ fn quality_is_identity(q: CoercionQuality) -> Bool { match q { Identity => true Exact => false + Widened => false } } data witness_find_witness_identity_accepts: Bool = match find_witness( diff --git a/src/v4/test/claim/manual/mvp_int_cross_target_coercion.dag b/src/v4/test/claim/manual/mvp_int_cross_target_coercion.dag index 1b10459b89b..a12a8d0a86d 100644 --- a/src/v4/test/claim/manual/mvp_int_cross_target_coercion.dag +++ b/src/v4/test/claim/manual/mvp_int_cross_target_coercion.dag @@ -1,20 +1,28 @@ // src/v4/test/claim/manual/mvp_int_cross_target_coercion.dag -// Scope: W3 Leg A — cross-target coercion_fold fail-closed safety receipt (python unbounded int → rust i32). -// Status: exact-structural preservation only; no silent width truncation until W3.2 widening rule lands. +// Scope: W3 cross-target int coercion receipts — Leg A fail-closed (python int → rust i32 exact rule); +// Leg B faithful widening (rust i32 → python int via preservation_rule_refinement_widening). module v4.test.claim.manual.mvp_int_cross_target_coercion import v4.compiler.eval { run_test_claim_assert } -import v4.extdeps.languages.python { python_int_inhabitant_node } +import v4.extdeps.languages.python { + python_declared_inhabitants_root, + python_int_inhabitant_node +} import v4.extdeps.languages.rust { rust_declared_inhabitants_root, rust_inhabitant_i32_node } +import v4.extdeps.coercion_widening { coercion_fold_mvp_rust_i32_to_python_int_widening } import v4.std.coercion { + CoercionQuality, CoercionResult, + Exact, + Identity, NoTargetCandidate, + Widened, coercion_candidate_set_from_declared_inhabitants, coercion_fold, coercion_not_realized_diagnostic @@ -163,3 +171,75 @@ data claim_cross_target_python_to_rust_i32_rejects_compiles: TestClaim = Compile expected_value: python_int_inhabitant_node(), classification: TestClassification { tier: Tier1, layer: Unit } } + + +fn rust_i32_grounding() -> CanonicalGrounding { + let source = rust_inhabitant_i32_node() + CanonicalGrounding { + node: source, + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: constraint_property_being_canonical, + evidence: source + }, + closedness: StructuralPropertyWitness { + property: constraint_property_candidate_set_closedness, + evidence: source + } + } + } +} + + +fn cross_target_rust_i32_to_python_int_coercion_fold() -> Outcome { + bind_outcome( + o: coercion_candidate_set_from_declared_inhabitants( + inhabitants_root: python_declared_inhabitants_root(), + closedness_property: target_model_edge_declared_inhabitants + ), + f: fn(candidates) { + coercion_fold_mvp_rust_i32_to_python_int_widening( + source: rust_i32_grounding(), + candidates: candidates, + priority: python_int_inhabitant_node() + ) + } + ) +} + + +fn quality_is_widened(q: CoercionQuality) -> Bool { + match q { + Widened => true + Identity => false + Exact => false + } +} + + +fn witness_cross_target_rust_i32_to_python_int_accepts() -> Bool { + let outcome = cross_target_rust_i32_to_python_int_coercion_fold() + match outcome { + Accepted { value: r, diagnostics: _ } => + (r.target == python_int_inhabitant_node()) && quality_is_widened(q: r.quality) + Rejected { diagnostics: _ } => false + } +} + + +fn cross_target_widening_witness_claim_input(ok: Bool) -> Node { + if ok { + rust_inhabitant_i32_node() + } else { + python_int_inhabitant_node() + } +} + + +data claim_cross_target_rust_i32_to_python_int_accepts: TestClaim = CompilesClaim { + label: "manual/mvp_int_cross_target: rust i32 -> python int coercion_fold_refinement_widening accepts Widened", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + input: cross_target_widening_witness_claim_input(ok: witness_cross_target_rust_i32_to_python_int_accepts()), + expected_value: python_int_inhabitant_node(), + classification: TestClassification { tier: Tier1, layer: Unit } +}