diff --git a/src/v4/compiler/04_infer.dag b/src/v4/compiler/04_infer.dag index e7fa3d1ef1f..9f1ca1f9333 100644 --- a/src/v4/compiler/04_infer.dag +++ b/src/v4/compiler/04_infer.dag @@ -5,7 +5,7 @@ module v4.compiler.infer -import v4.std.algebra { list_snoc_item } +import v4.std.algebra { length, list_snoc_item } // kernel-mark: SG-6 gate imports โ€” `_bounded` substring is BoundedLattice domain naming, not Practice-12 fuel. import v4.std.bounded_lattice_completeness { infer_bounded_lattice_consumer_gate, @@ -13,7 +13,13 @@ import v4.std.bounded_lattice_completeness { } import v4.compiler.resolve { ResolvedTree } import v4.std.cardinality { TerminationProof, termination_proof_witness_for_node } -import v4.std.collection { List, Map } +import v4.std.collection { + Absent, + List, + Map, + Present, + list_at_optional +} import v4.std.constraints { CanonicalGrounding, CanonicalGroundingWitness, @@ -35,21 +41,25 @@ import v4.std.diagnostic { diagnostics_merge, diagnostics_singleton, outcome_rejected, - outcome_accepted, rejected_with_pending } -import v4.std.logic { Bool } +import v4.std.logic { Bool, bool_node } import v4.std.node { Atom, + Branch, ComputationNode, + Edge, Node, NodeFold, Symbol, + SyntheticOccurrence, TypeNode, + all_edges_positional, fold_node, well_formed } -import v4.std.witness { Holds, Violates, Witness } +import v4.std.node_query { node_positional_child_targets } +import v4.std.witness { Holds, StructuralPropertyWitness, Violates, Witness } // AlgebraRef is the typed IR-1 bridge for algebra inhabitance coordinates. type AlgebraRef { @@ -93,11 +103,22 @@ type InferredFactsEntry { facts: InferredFacts } +// Named fold carrier โ€” avoids nested Outcome> in gather init (parser). +type InferGatherFoldAcc { + entries: List + failed: Bool + pending: Diagnostics +} + data infer_descent_not_derived: Symbol = infer_descent_not_derived data infer_facts_lookup_miss: Symbol = infer_facts_lookup_miss data infer_canonical_grounding_incoherent: Symbol = infer_canonical_grounding_incoherent // ๐ŸŸข SM5-satisfied: v2 bootstrap on src/v4 emits 0 infer_algebra_ref_ungrounded diagnostics (2026-05-26); guard dissolves when T-4 Wave 2b/T-2 populate AlgebraRef from grounded algebra Node constructors. data infer_algebra_ref_ungrounded: Symbol = infer_algebra_ref_ungrounded +data infer_branch_shape_invalid: Symbol = infer_branch_shape_invalid +data infer_branch_cond_not_bool: Symbol = infer_branch_cond_not_bool +data infer_branch_arm_type_mismatch: Symbol = infer_branch_arm_type_mismatch +data infer_gather_fold_failure: Symbol = infer_gather_fold_failure // ยง1-tail A4 disposition (post-#4692): Practice-12 `_bounded` fuel residue = 0 in this stage. // SG-6 BoundedLattice gather/gate โ†’ fuel-delete: rows in v4.std.bounded_lattice_completeness @@ -127,6 +148,30 @@ fn infer_algebra_ref_ungrounded_diagnostic(node: Node) -> Diagnostic { } } +fn infer_branch_shape_invalid_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: infer_branch_shape_invalid, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn infer_branch_cond_not_bool_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: infer_branch_cond_not_bool, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn infer_branch_arm_type_mismatch_diagnostic(node: Node) -> Diagnostic { + Diagnostic { + reason: infer_branch_arm_type_mismatch, + at: node_locus(node: node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + // ๐ŸŸก gated โ€” feature:infer-algebra-ref-grounding-fold โ€” bind v4.compiler.infer://algebra-ref-grounded โ€” dissolve-on-arrival: std/node.dag or std/model_core.dag exports the canonical grounded-algebra query. fn algebra_ref_is_grounded(algebra: Node) -> Bool { match algebra.kind { @@ -219,6 +264,23 @@ fn infer_constraint_graph(n: Node) -> ConstraintGraph { ConstraintGraph { root: n } } +// ๐ŸŸก gated โ€” feature:branch-infer-constraint-solve-bridge โ€” +// bind:github.com/gunb-ai/gunbc#4772 โ€” +// dissolve-on: solve_constraints emits being_canonical at source; delete infer_grounding_from_constraint_solve. +fn infer_grounding_from_constraint_solve(grounding: CanonicalGrounding) -> CanonicalGrounding { + CanonicalGrounding { + node: grounding.node, + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: ^constraint_property_being_canonical, + evidence: grounding.witness.structural.evidence + }, + closedness: grounding.witness.closedness + } + } +} + +// Route-scoped bridge: only infer_node_facts โ†’ solve_constraints calls this remapper. fn infer_node_facts(n: Node, partials: List) -> Outcome { match infer_bounded_lattice_consumer_gate(consumer: n, partials: partials) { Rejected { diagnostics: r } => Rejected { diagnostics: r } @@ -235,7 +297,7 @@ fn infer_node_facts(n: Node, partials: List) -> Outcome { ), f: fn(grounding) { inferred_facts_from_grounding( - grounding: grounding, + grounding: infer_grounding_from_constraint_solve(grounding: grounding), descent: Holds { value: descent_proof } ) } @@ -344,47 +406,345 @@ fn admitted_inferred_facts_entry(node: Node, facts: InferredFacts) -> Outcome Outcome> { - let partials = partial_bounded_lattice_instances_in_tree(tree: tree) - fold_node( - n: tree, - algebra: NodeFold { - init: fn(n0) { - match infer_node_facts(n: n0, partials: partials) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: facts, diagnostics: d } => - match admitted_inferred_facts_entry(node: n0, facts: facts) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: entry, diagnostics: ed } => - Accepted { - value: [entry], - diagnostics: diagnostics_merge(outer: d, inner: ed) +fn infer_branch_int_binding_type_node() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: ^dag_binding_type_int } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn infer_branch_is_bool_literal_atom(node: Node) -> Bool { + match node.kind { + TypeNode { connective: Atom { identity: id } } => + (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false) + _ => false + } +} + +fn infer_branch_is_int_literal_atom(node: Node) -> Bool { + match node.kind { + TypeNode { connective: Atom { identity: id } } => + (id == ^dag_mvp1_pick_lit_one) || (id == ^dag_mvp1_pick_lit_two) + _ => false + } +} + +// ๐ŸŸก gated โ€” branch infer M0 literal operand typing โ€” feature:branch-infer-literal-types โ€” +// bind:docs/design-comprep-m0-branch-mapping.md ยง12.11 Q-B2 โ€” dissolve-on: github.com/gunb-ai/gunbc#4772 constraint carriers at infer_node_facts +// assign literal operand types during infer_node_facts instead of Branch-row semantic projection. +fn infer_branch_operand_resolved_type(node: Node, facts: InferredFacts) -> Node { + if infer_branch_is_bool_literal_atom(node: node) { + bool_node() + } else if infer_branch_is_int_literal_atom(node: node) { + infer_branch_int_binding_type_node() + } else { + inferred_facts_resolved_type(facts: facts) + } +} + +fn infer_branch_canonical_grounding(node: Node, unified_type: Node) -> CanonicalGrounding { + CanonicalGrounding { + node: node, + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: ^constraint_property_being_canonical, + evidence: unified_type + }, + closedness: StructuralPropertyWitness { + property: ^constraint_property_candidate_set_closedness, + evidence: node + } + } + } +} + +fn infer_branch_type_atoms_equal(a: Node, b: Node) -> Bool { + match a.kind { + TypeNode { connective: Atom { identity: id_a } } => + match b.kind { + TypeNode { connective: Atom { identity: id_b } } => id_a == id_b + _ => false + } + _ => a == b + } +} + +fn infer_branch_type_is_bool(type_node: Node) -> Bool { + match type_node.kind { + TypeNode { connective: Atom { identity: id } } => id == ^bool_node_symbol + _ => false + } +} + +fn infer_unify_branch_arm_types( + then_node: Node, + then_facts: InferredFacts, + else_node: Node, + else_facts: InferredFacts, +) -> Outcome { + let then_type = infer_branch_operand_resolved_type(node: then_node, facts: then_facts) + let else_type = infer_branch_operand_resolved_type(node: else_node, facts: else_facts) + if infer_branch_type_atoms_equal(a: then_type, b: else_type) { + Accepted { value: then_type, diagnostics: None } + } else { + outcome_rejected(infer_branch_arm_type_mismatch_diagnostic(node: then_node)) + } +} + +// Q-B2 gather-algebra row: Bool-if-else Branch โ€” cond child typed Bool; arms unify to Branch result type. +fn infer_branch_bool_if_else( + node: Node, + partials: List, + entries: List, +) -> Outcome { + let positional_targets = node_positional_child_targets(node: node) + if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { + outcome_rejected(infer_branch_shape_invalid_diagnostic(node: node)) + } else { + match list_at_optional(xs: positional_targets, index: 0) { + Absent => outcome_rejected(infer_branch_shape_invalid_diagnostic(node: node)) + Present { value: cond_target } => + match list_at_optional(xs: positional_targets, index: 1) { + Absent => outcome_rejected(infer_branch_shape_invalid_diagnostic(node: node)) + Present { value: then_target } => + match list_at_optional(xs: positional_targets, index: 2) { + Absent => outcome_rejected(infer_branch_shape_invalid_diagnostic(node: node)) + Present { value: else_target } => + match lookup_inferred_facts_in_entries(entries: entries, key: cond_target) { + Violates { diagnostic: d } => outcome_rejected(d) + Holds { value: cond_facts } => + match lookup_inferred_facts_in_entries(entries: entries, key: then_target) { + Violates { diagnostic: d } => outcome_rejected(d) + Holds { value: then_facts } => + match lookup_inferred_facts_in_entries(entries: entries, key: else_target) { + Violates { diagnostic: d } => outcome_rejected(d) + Holds { value: else_facts } => + match infer_bounded_lattice_consumer_gate(consumer: node, partials: partials) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: _, diagnostics: cd } => + if !infer_branch_type_is_bool( + type_node: infer_branch_operand_resolved_type( + node: cond_target, + facts: cond_facts + ) + ) { + outcome_rejected(infer_branch_cond_not_bool_diagnostic(node: node)) + } else { + match infer_unify_branch_arm_types( + then_node: then_target, + then_facts: then_facts, + else_node: else_target, + else_facts: else_facts + ) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: unified_type, diagnostics: ud } => + match infer_descent_witness_for_node(n: node) { + Violates { diagnostic: d } => + Rejected { diagnostics: diagnostics_singleton(d: d) } + Holds { value: descent_proof } => + bind_outcome( + o: inferred_facts_from_grounding( + grounding: infer_branch_canonical_grounding( + node: node, + unified_type: unified_type + ), + descent: Holds { value: descent_proof } + ), + f: fn(facts) { + Accepted { + value: facts, + diagnostics: diagnostics_merge(outer: cd, inner: ud) + } + } + ) + } + } + } + } + } + } } } } - }, - step: fn(acc, e, child) { - match acc { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: acc_entries, diagnostics: ad } => - match child { - Rejected { diagnostics: cr } => - Rejected { - diagnostics: rejected_with_pending(pending: ad, rejected: cr) - } - Accepted { value: child_entries, diagnostics: cd } => - Accepted { - value: concat_inferred_facts_entries(a: acc_entries, b: child_entries), - diagnostics: diagnostics_merge(outer: ad, inner: cd) - } + } + } +} + +fn infer_gather_fold_acc_failed(pending: NonEmptyDiagnostics) -> InferGatherFoldAcc { + InferGatherFoldAcc { + entries: empty_inferred_facts_entry_list(), + failed: true, + pending: Some { diagnostics: pending } + } +} + +fn infer_gather_fold_acc_ok( + entries: List, + pending: Diagnostics, +) -> InferGatherFoldAcc { + InferGatherFoldAcc { + entries: entries, + failed: false, + pending: pending + } +} + +fn infer_gather_acc_to_outcome(acc: InferGatherFoldAcc) -> Outcome> { + if acc.failed { + match acc.pending { + None => + Rejected { + diagnostics: diagnostics_singleton( + d: infer_canonical_grounding_incoherent_diagnostic(node: infer_gather_fold_failure_node()) + ) + } + Some { diagnostics: nds } => Rejected { diagnostics: nds } + } + } else { + Accepted { + value: acc.entries, + diagnostics: acc.pending + } + } +} + +fn infer_gather_fold_failure_node() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: ^infer_gather_fold_failure } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn infer_gather_replace_entry_for_node( + entries: List, + node: Node, + replacement: InferredFactsEntry, +) -> List { + fold(entries, init: empty_inferred_facts_entry_list(), f: fn(acc, entry) { + if entry.node == node { + list_snoc_item(xs: acc, item: replacement) + } else { + list_snoc_item(xs: acc, item: entry) + } + }) +} + +fn infer_gather_apply_branch_row( + n: Node, + acc: InferGatherFoldAcc, + partials: List, +) -> InferGatherFoldAcc { + if acc.failed { + acc + } else { + match n.kind { + ComputationNode { behavior: Branch } => + match infer_branch_bool_if_else(node: n, partials: partials, entries: acc.entries) { + Rejected { diagnostics: r } => + infer_gather_fold_acc_failed( + pending: rejected_with_pending(pending: acc.pending, rejected: r) + ) + Accepted { value: facts, diagnostics: d } => + match admitted_inferred_facts_entry(node: n, facts: facts) { + Rejected { diagnostics: r } => + infer_gather_fold_acc_failed( + pending: rejected_with_pending(pending: acc.pending, rejected: r) + ) + Accepted { value: entry, diagnostics: ed } => + infer_gather_fold_acc_ok( + entries: infer_gather_replace_entry_for_node( + entries: acc.entries, + node: n, + replacement: entry + ), + pending: diagnostics_merge( + outer: diagnostics_merge(outer: acc.pending, inner: d), + inner: ed + ) + ) } } + _ => acc + } + } +} + +fn infer_gather_fold_init(n: Node, partials: List) -> InferGatherFoldAcc { + match infer_node_facts(n: n, partials: partials) { + Rejected { diagnostics: r } => infer_gather_fold_acc_failed(pending: r) + Accepted { value: facts, diagnostics: d } => + match admitted_inferred_facts_entry(node: n, facts: facts) { + Rejected { diagnostics: r } => infer_gather_fold_acc_failed(pending: r) + Accepted { value: entry, diagnostics: ed } => + infer_gather_fold_acc_ok( + entries: [entry], + pending: diagnostics_merge(outer: d, inner: ed) + ) } + } +} + +fn infer_gather_failed_non_empty(acc: InferGatherFoldAcc) -> NonEmptyDiagnostics { + match acc.pending { + Some { diagnostics: nds } => nds + None => + diagnostics_singleton( + d: infer_canonical_grounding_incoherent_diagnostic(node: infer_gather_fold_failure_node()) + ) + } +} + +fn infer_gather_fold_step( + acc: InferGatherFoldAcc, + edge: Edge, + child: InferGatherFoldAcc, +) -> InferGatherFoldAcc { + if acc.failed { + acc + } else if child.failed { + infer_gather_fold_acc_failed( + pending: rejected_with_pending( + pending: acc.pending, + rejected: infer_gather_failed_non_empty(acc: child) + ) + ) + } else { + infer_gather_fold_acc_ok( + entries: concat_inferred_facts_entries(a: acc.entries, b: child.entries), + pending: diagnostics_merge(outer: acc.pending, inner: child.pending) + ) + } +} + +fn infer_gather_fold_algebra(partials: List) -> NodeFold { + NodeFold { + init: fn(n0) { + infer_gather_fold_init(n: n0, partials: partials) + }, + step: fn(acc, e, child) { + infer_gather_fold_step(acc: acc, edge: e, child: child) } + } +} + +fn infer_gather_fold_node(n: Node, partials: List) -> InferGatherFoldAcc { + infer_gather_apply_branch_row( + n: n, + acc: fold_node(n: n, algebra: infer_gather_fold_algebra(partials: partials)), + partials: partials ) } +fn infer_grounding_admits_infer_facts(grounding: CanonicalGrounding) -> Bool { + canonical_grounding_admits_infer_facts(grounding: grounding) +} + +fn infer_entries_for_tree(tree: ResolvedTree) -> Outcome> { + let partials = partial_bounded_lattice_instances_in_tree(tree: tree) + infer_gather_acc_to_outcome(acc: infer_gather_fold_node(n: tree, partials: partials)) +} fn infer(tree: ResolvedTree) -> Outcome { match infer_entries_for_tree(tree: tree) { Rejected { diagnostics: r } => Rejected { diagnostics: r } diff --git a/src/v4/test/claim/manual/branch_infer.dag b/src/v4/test/claim/manual/branch_infer.dag new file mode 100644 index 00000000000..6efe6fbe949 --- /dev/null +++ b/src/v4/test/claim/manual/branch_infer.dag @@ -0,0 +1,205 @@ +// src/v4/test/claim/manual/branch_infer.dag +// Scope: Q-B2 โ€” 04_infer Branch row discriminating claims (Bool cond + arm unification). +// Status: infer half โ€” docs/design-comprep-m0-branch-mapping.md ยง12.11. + +module v4.test.claim.manual.branch_infer + +import v4.compiler.infer { + infer, + infer_branch_operand_resolved_type, + infer_branch_type_atoms_equal, + infer_branch_type_is_bool, + infer_grounding_admits_infer_facts, + inferred_facts_resolved_type, + inferred_facts_witness_for_node, + InferredTree +} +import v4.compiler.resolve { ResolvedTree } +import v4.std.collection { Absent, List, Present, list_at_optional } +import v4.std.constraints { CanonicalGrounding, CanonicalGroundingWitness } +import v4.std.diagnostic { Accepted, Outcome, Rejected } +import v4.std.find_witness { preservation_rule_constraint_satisfaction } +import v4.std.logic { Bool } +import v4.std.node { + Atom, + Branch, + ComputationNode, + Edge, + Node, + Positional, + Symbol, + SyntheticOccurrence, + TypeNode +} +import v4.std.node_query { node_positional_child_targets } +import v4.std.verification { + BoolWitness, + BoolWitnessClaim, + ManualAnchorAbsent, + UnifiedTestClaim +} +import v4.std.witness { Holds, StructuralPropertyWitness, Violates } + +fn branch_infer_atom(s: Symbol) -> Node { + Node { + kind: TypeNode { connective: Atom { identity: s } }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn branch_infer_int_binding_type_node() -> Node { + branch_infer_atom(s: ^dag_binding_type_int) +} + +fn branch_infer_string_type_node() -> Node { + branch_infer_atom(s: ^branch_infer_string_type) +} + +fn branch_infer_if_body_from_arms( + condition: Node, + then_arm: Node, + else_arm: Node +) -> Node { + Node { + kind: ComputationNode { behavior: Branch }, + children: [ + Edge { label: Positional, target: condition }, + Edge { label: Positional, target: then_arm }, + Edge { label: Positional, target: else_arm } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn branch_infer_bool_if_else_body_node() -> Node { + branch_infer_if_body_from_arms( + condition: branch_infer_atom(s: ^dag_token_kw_true), + then_arm: branch_infer_atom(s: ^dag_mvp1_pick_lit_one), + else_arm: branch_infer_atom(s: ^dag_mvp1_pick_lit_two) + ) +} + +fn branch_infer_arm_mismatch_body_node() -> Node { + branch_infer_if_body_from_arms( + condition: branch_infer_atom(s: ^dag_token_kw_true), + then_arm: branch_infer_atom(s: ^dag_mvp1_pick_lit_one), + else_arm: branch_infer_string_type_node() + ) +} + +fn branch_infer_cond_not_bool_body_node() -> Node { + branch_infer_if_body_from_arms( + condition: branch_infer_atom(s: ^dag_mvp1_pick_lit_one), + then_arm: branch_infer_atom(s: ^dag_mvp1_pick_lit_one), + else_arm: branch_infer_atom(s: ^dag_mvp1_pick_lit_two) + ) +} + +fn branch_infer_resolved_tree(root: Node) -> ResolvedTree { + root +} + +fn branch_infer_positional_target(body: Node, index: Int) -> Node { + match list_at_optional(xs: node_positional_child_targets(node: body), index: index) { + Present { value: target } => target + Absent => branch_infer_atom(s: ^branch_infer_missing_child) + } +} + +fn branch_infer_run(tree: ResolvedTree) -> Outcome { + infer(tree: tree) +} + +fn branch_infer_cond_child_is_bool(tree: InferredTree, body: Node) -> Bool { + let cond = branch_infer_positional_target(body: body, index: 0) + match inferred_facts_witness_for_node(tree: tree, node: cond) { + Holds { value: facts } => + infer_branch_type_is_bool( + type_node: infer_branch_operand_resolved_type(node: cond, facts: facts) + ) + Violates { diagnostic: _ } => false + } +} + +fn branch_infer_branch_result_is_int(tree: InferredTree, body: Node) -> Bool { + match inferred_facts_witness_for_node(tree: tree, node: body) { + Holds { value: facts } => + infer_branch_type_atoms_equal( + a: inferred_facts_resolved_type(facts: facts), + b: branch_infer_int_binding_type_node() + ) + Violates { diagnostic: _ } => false + } +} + +fn branch_infer_bool_cond_accepts_holds() -> Bool { + let body = branch_infer_bool_if_else_body_node() + let tree = branch_infer_resolved_tree(root: body) + match branch_infer_run(tree: tree) { + Accepted { value: inferred, diagnostics: _ } => + branch_infer_cond_child_is_bool(tree: inferred, body: body) + && branch_infer_branch_result_is_int(tree: inferred, body: body) + Rejected { diagnostics: _ } => false + } +} + +fn branch_infer_arm_mismatch_red_holds() -> Bool { + let body = branch_infer_arm_mismatch_body_node() + match branch_infer_run(tree: branch_infer_resolved_tree(root: body)) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +fn branch_infer_cond_not_bool_red_holds() -> Bool { + let body = branch_infer_cond_not_bool_body_node() + match branch_infer_run(tree: branch_infer_resolved_tree(root: body)) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +fn branch_infer_keystone_holds() -> Bool { + branch_infer_bool_cond_accepts_holds() + && branch_infer_arm_mismatch_red_holds() + && branch_infer_cond_not_bool_red_holds() +} + +// Negative witness: preservation_rule grounding is still rejected by the admission gate +// outside the infer_node_facts โ†’ solve_constraints bridge remapper. +fn branch_infer_constraint_satisfaction_grounding_rejected() -> CanonicalGrounding { + CanonicalGrounding { + node: branch_infer_atom(s: ^branch_infer_constraint_satisfaction_node), + witness: CanonicalGroundingWitness { + structural: StructuralPropertyWitness { + property: preservation_rule_constraint_satisfaction, + evidence: branch_infer_atom(s: ^branch_infer_constraint_satisfaction_evidence) + }, + closedness: StructuralPropertyWitness { + property: ^constraint_property_candidate_set_closedness, + evidence: branch_infer_atom(s: ^branch_infer_constraint_satisfaction_node) + } + } + } +} + +fn branch_infer_admission_gate_rejects_constraint_satisfaction_holds() -> Bool { + !infer_grounding_admits_infer_facts( + grounding: branch_infer_constraint_satisfaction_grounding_rejected() + ) +} + +data unified_claim_branch_infer: UnifiedTestClaim = BoolWitnessClaim { + witness: BoolWitness { + entry: "src/v4/test/claim/manual/branch_infer.dag", + function: branch_infer_keystone_holds + } +} + +data unified_claim_branch_infer_admission_gate: UnifiedTestClaim = BoolWitnessClaim { + witness: BoolWitness { + entry: "src/v4/test/claim/manual/branch_infer.dag", + function: branch_infer_admission_gate_rejects_constraint_satisfaction_holds + } +}