diff --git a/dag/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 5987274ec36..641e52eb96a 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -1550,7 +1550,6 @@ data non_fold_residue_frontier: List = [ FrontierRow { subject: PathSubject { path: "src/v2/compiler/04_infer.dag::infer_match_bool_arm_row" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "src/v2/compiler/04_infer.dag::infer_operator_arrow" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "src/v2/compiler/04_infer.dag::infer_sum_nullary_payload_edge" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, - FrontierRow { subject: PathSubject { path: "src/v2/compiler/04_infer.dag::infer_transform_operator_is_int_add" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "src/v2/compiler/05_emit_orchestration.dag::orch_emit_retry_1level" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "src/v2/compiler/05_emit_orchestration.dag::orch_emit_retry_levels" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "src/v2/compiler/05_eval.dag::eval_binding_key_from_atom" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 7a6873905ba..26738cfeed3 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -11,6 +11,9 @@ import v2.std.bounded_lattice_completeness { partial_bounded_lattice_instances_in_tree } import v2.std.compilers.target_model { + AlgebraPrimitive, + CanonicalOperation, + canonical_operation_from_wire_node, canonical_operation_op_add, canonical_operation_op_coerce, canonical_operation_wire_matches_operation, @@ -26,7 +29,11 @@ import v2.compiler.inferred_tree { ObligatedInferredTree, NodeGrounding } +import v2.std.algebra_structure_signature { FieldDeclared, FieldNotDeclared, InhabitanceFieldRead, InhabitanceFieldReadMalformed, InhabitanceMalformed, algebra_inhabitance_field_reading } +import v2.std.model_core { AlgebraInhabitanceDecl } +import v2.std.grammar { node_atom_identity_optional } import v2.extdeps.languages.dag { + dag_algebra_inhabitance_decls, DagCanonicalBoolLiteral, DagCanonicalIntLiteral, DagCanonicalSymbolLiteral, @@ -2851,39 +2858,108 @@ fn infer_loop_iteration( } } -// First behavior-specific Transform derivation (v2-inferred-tree-completeness): binary infix Int -// add derives the unified Int type as the expression result — the add_probe body vertical. Operator -// recognition accepts dag_token_plus pre-resolve and the canonical add operation wire post-resolve -// (03_resolve.resolve_transform_operator_child). Every reached Transform awaits the transform row -// so application-argument inhabitance runs; add-shape result derivation is selected inside -// infer_gather_transform_row_on_entries, and non-add Transforms stay GroundingNotDerived as the -// application's result type after the inhabitance judgment. dissolve-on: general operator/operand -// typing table subsumes the add-only result rule. +// Binary algebra-operator derivation (v2-inferred-tree-completeness): a binary infix Transform whose +// operator is an algebra primitive derives its result through the operand type's structure, by the one +// route below (infer_binary_algebra_field, infer_algebra_field_result_type) -- `+` and `||` alike, with no +// per-operator or per-type arm. Operator recognition accepts dag_token_plus pre-resolve and the canonical +// operation wire post-resolve (03_resolve.resolve_transform_operator_child). Every reached Transform awaits +// the transform row so application-argument inhabitance runs; this derivation is selected inside +// infer_gather_transform_row_on_entries, and a Transform that is not a binary algebra primitive stays +// GroundingNotDerived as the application's result type after the inhabitance judgment. + +// A BINARY ALGEBRA OPERATOR NAMES ONE FIELD OF A STRUCTURE, and the field is the whole of what it says: the +// lowered operator is a canonical-operation wire (v2.std.compilers.target_model canonical_operation_from_wire_node) +// whose AlgebraPrimitive carries the signature field -- ^ring_field_add for `+`, ^lattice_field_join for `||`, +// ^lattice_field_meet for `&&`. The bare `+` token is the add field's surface spelling +// (canonical_operation_op_add). Anything else is not an algebra primitive and stays out of this arm. +fn infer_binary_algebra_field(op_node: Node) -> Optional { + if infer_operator_is_plus_token(op_node: op_node) { + infer_canonical_operation_field(operation: canonical_operation_op_add()) + } else { + infer_wire_algebra_field(wire: op_node) + } +} -fn infer_transform_operator_is_int_add(op_node: Node) -> Bool { - match op_node.kind { - TypeNode { connective: Atom { identity: id } } => - id == ^dag_token_plus - || canonical_operation_wire_matches_operation( - wire: op_node, - operation: canonical_operation_op_add() - ) - _ => - canonical_operation_wire_matches_operation( - wire: op_node, - operation: canonical_operation_op_add() - ) +fn infer_operator_is_plus_token(op_node: Node) -> Bool { + match node_atom_identity_optional(node: op_node) { + Present { value: id } => id == ^dag_token_plus + Absent => false + } +} + +fn infer_wire_algebra_field(wire: Node) -> Optional { + match canonical_operation_from_wire_node(wire: wire) { + Accepted { value: decoded, diagnostics: _ } => infer_canonical_operation_field(operation: decoded) + Rejected { diagnostics: _ } => optional_absent() + } +} + +fn infer_canonical_operation_field(operation: CanonicalOperation) -> Optional { + match operation { + AlgebraPrimitive { algebra_field: field } => optional_present(value: field) + AlgebraInverseCompose { binary_field: _, inverse_field: _ } => optional_absent() + OrderingComparison { compare_field: _, predicate: _ } => optional_absent() + EqualityComparison { eq_field: _, predicate: _ } => optional_absent() + CoercionCrossing { homomorphism_rule: _ } => optional_absent() } } -fn infer_transform_is_binary_infix_int_add_shape(node: Node) -> Bool { +// THE OPERAND TYPE CARRIES THE FIELD WHEN ITS LANGUAGE MODEL SAYS SO: a row in +// v2.extdeps.languages.dag dag_algebra_inhabitance_decls inhabits a structure that DECLARES the field, read +// through v2.std.algebra_structure_signature algebra_inhabitance_field_reading (the structure's binders and +// the sub-structures it composes -- never a name found inside an operation's signature). The row is SELECTED by +// the carrier its own inhabitance node is over (the ^inhabitant_edge target, read in the same call), never by the +// row's outer `inhabitant` field: that field is a second copy of the carrier, and selecting by it let a row whose +// copy disagreed with its structure lend the structure's fields to a type the structure is not over. The result is the +// operand type because every binary algebra primitive these structures carry is closed on the carrier: a +// lattice join is algebra_binary_fn_node(domain: T, T, codomain: T), and ring add is the operation of the +// abelian group the ring composes. This replaces the Int-only arm that hard-coded `+` over +// ^dag_binding_type_int: Int add derives through Int's ordered-ring row and Bool join through Bool's +// boolean-algebra row, by one route; a type with no row declaring the field (Bool `+`, Int `||`) is refused as +// an operand mismatch exactly as a non-Int `+` was. +// What the operand type's row answers for the field: the result type, no row carrying it, or a row whose +// inhabitance node is malformed -- the last refused with ITS cause, never as an operand mismatch. +type InferAlgebraFieldResult + = AlgebraFieldResultType { result: Node } + | AlgebraFieldNotCarried + | AlgebraFieldRowMalformed { cause: Symbol } + +fn infer_algebra_field_result_type(rows: List, operand_type: Node, field: Symbol) -> InferAlgebraFieldResult { + fold(rows, init: AlgebraFieldNotCarried, f: fn(acc, decl) { + match acc { + AlgebraFieldResultType { result: _ } => acc + AlgebraFieldRowMalformed { cause: _ } => acc + AlgebraFieldNotCarried => + match algebra_inhabitance_field_reading(inhabitance: decl.algebra, field: field) { + InhabitanceFieldReadMalformed { cause: c } => AlgebraFieldRowMalformed { cause: c } + InhabitanceFieldRead { carrier: carrier, declaration: declaration } => + if infer_branch_type_atoms_equal(a: carrier, b: operand_type) { + match declaration { + FieldDeclared => AlgebraFieldResultType { result: operand_type } + FieldNotDeclared => AlgebraFieldNotCarried + InhabitanceMalformed { cause: c } => AlgebraFieldRowMalformed { cause: c } + } + } else { + AlgebraFieldNotCarried + } + } + } + }) +} + + +fn infer_transform_is_binary_infix_algebra_shape(node: Node) -> Bool { let positional_targets = node_positional_child_targets(node: node) if !all_edges_positional(children: node.children) || length(xs: positional_targets) != 3 { false } else { match list_at_optional(xs: positional_targets, index: 0) { Absent => false - Present { value: op_target } => infer_transform_operator_is_int_add(op_node: op_target) + Present { value: op_target } => + match infer_binary_algebra_field(op_node: op_target) { + Present { value: _ } => true + Absent => false + } } } } @@ -3528,9 +3604,9 @@ fn infer_transform_binary_infix( match list_at_optional(xs: positional_targets, index: 2) { Absent => outcome_rejected(infer_transform_shape_invalid_diagnostic(node: node)) Present { value: right_target } => - if !infer_transform_operator_is_int_add(op_node: op_target) { - outcome_rejected(infer_transform_operator_unsupported_diagnostic(node: node)) - } else { + match infer_binary_algebra_field(op_node: op_target) { + Absent => outcome_rejected(infer_transform_operator_unsupported_diagnostic(node: node)) + Present { value: field } => match lookup_inferred_facts_in_entries(entries: entries, key: left_target) { Absent => outcome_rejected(infer_facts_lookup_miss_diagnostic(key: left_target)) Present { value: left_facts } => @@ -3550,11 +3626,18 @@ fn infer_transform_binary_infix( ) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: unified_type, diagnostics: ud } => - if !infer_branch_type_is_int(type_node: unified_type) { - outcome_rejected( - infer_transform_operand_type_mismatch_diagnostic(node: node) - ) - } else { + match infer_algebra_field_result_type(rows: dag_algebra_inhabitance_decls(), operand_type: unified_type, field: field) { + AlgebraFieldNotCarried => + outcome_rejected( + infer_transform_operand_type_mismatch_diagnostic(node: node) + ) + AlgebraFieldRowMalformed { cause: cause } => + outcome_rejected(Diagnostic { + reason: cause, + at: node_locus(node: node), + correction: Unavailable { reason: CorrectionNotModeled } + }) + AlgebraFieldResultType { result: result_type } => match infer_descent_witness_for_node(n: node) { Violates { diagnostic: d } => Rejected { diagnostics: diagnostics_singleton(d: d) } @@ -3562,7 +3645,7 @@ fn infer_transform_binary_infix( bind_outcome( o: inferred_facts_from_derived_type( node: node, - derived_type: unified_type, + derived_type: result_type, descent: Holds { value: descent_proof } ), f: fn(facts) { @@ -4164,7 +4247,7 @@ fn infer_transform_derived_optional( resolved: ResolvedTree, arguments_decided: Bool, ) -> Optional> { - if infer_transform_is_binary_infix_int_add_shape(node: node) { + if infer_transform_is_binary_infix_algebra_shape(node: node) { optional_present(value: infer_transform_binary_infix(node: node, partials: partials, entries: entries, resolved: resolved)) } else if infer_transform_is_cast(node: node) { infer_transform_cast_optional(node: node, entries: entries, resolved: resolved) diff --git a/src/v2/std/algebra_structure_signature.dag b/src/v2/std/algebra_structure_signature.dag index fd6ebd94d7e..29d47eef01d 100644 --- a/src/v2/std/algebra_structure_signature.dag +++ b/src/v2/std/algebra_structure_signature.dag @@ -313,19 +313,35 @@ type AlgebraFieldDeclaration | FieldNotDeclared | InhabitanceMalformed { cause: Symbol } -fn algebra_inhabitance_field_declaration(inhabitance: Node, field: Symbol) -> AlgebraFieldDeclaration { +// THE INHABITANCE'S CARRIER AND ITS ANSWER FOR ONE FIELD, READ TOGETHER FROM THE ONE NODE THAT STATES BOTH: the +// ^inhabitant_edge target IS the carrier the structure is over, so a consumer selecting an inhabitance by its +// carrier reads it here, and never from a second copy stored beside the node (which could disagree with it and +// would make the structure's fields answer for a type it is not over). +type AlgebraInhabitanceFieldReading + = InhabitanceFieldRead { carrier: Node, declaration: AlgebraFieldDeclaration } + | InhabitanceFieldReadMalformed { cause: Symbol } + +fn algebra_inhabitance_field_reading(inhabitance: Node, field: Symbol) -> AlgebraInhabitanceFieldReading { match named_child_lookup(root: inhabitance, name: ^inhabitant_edge) { - NamedChildMissing => InhabitanceMalformed { cause: ^algebra_inhabitance_inhabitant_edge_missing } - NamedChildAmbiguous => InhabitanceMalformed { cause: ^algebra_inhabitance_inhabitant_edge_ambiguous } - NamedChildFound { target: _ } => + NamedChildMissing => InhabitanceFieldReadMalformed { cause: ^algebra_inhabitance_inhabitant_edge_missing } + NamedChildAmbiguous => InhabitanceFieldReadMalformed { cause: ^algebra_inhabitance_inhabitant_edge_ambiguous } + NamedChildFound { target: carrier } => match named_child_lookup(root: inhabitance, name: ^algebra_edge) { - NamedChildMissing => InhabitanceMalformed { cause: ^algebra_inhabitance_algebra_edge_missing } - NamedChildAmbiguous => InhabitanceMalformed { cause: ^algebra_inhabitance_algebra_edge_ambiguous } - NamedChildFound { target: algebra } => algebra_structure_field_declaration(structure: algebra, field: field) + NamedChildMissing => InhabitanceFieldReadMalformed { cause: ^algebra_inhabitance_algebra_edge_missing } + NamedChildAmbiguous => InhabitanceFieldReadMalformed { cause: ^algebra_inhabitance_algebra_edge_ambiguous } + NamedChildFound { target: algebra } => + InhabitanceFieldRead { carrier: carrier, declaration: algebra_structure_field_declaration(structure: algebra, field: field) } } } } +fn algebra_inhabitance_field_declaration(inhabitance: Node, field: Symbol) -> AlgebraFieldDeclaration { + match algebra_inhabitance_field_reading(inhabitance: inhabitance, field: field) { + InhabitanceFieldReadMalformed { cause: c } => InhabitanceMalformed { cause: c } + InhabitanceFieldRead { carrier: _, declaration: d } => d + } +} + // THE STRUCTURE IS READ AS WHAT IT MUST BE, AND ANY OTHER SHAPE IS MALFORMED -- never a plausible answer. A // structure is a Conj whose every child is an Authored BINDER; a field is declared only by a binder (a matching // name on a non-binder edge is malformed, not declared); a composing field must carry a structure (a composing diff --git a/src/v2/test/claim/algebra_operator_derivation_test.dag b/src/v2/test/claim/algebra_operator_derivation_test.dag new file mode 100644 index 00000000000..eb150a5170f --- /dev/null +++ b/src/v2/test/claim/algebra_operator_derivation_test.dag @@ -0,0 +1,140 @@ +module v2.test.claim.algebra_operator_derivation + +import v2.compiler.infer { AlgebraFieldNotCarried, AlgebraFieldResultType, AlgebraFieldRowMalformed, InferAlgebraFieldResult, infer, infer_algebra_field_result_type } +import v2.std.algebra_structure_signature { boolean_algebra_node, ordered_ring_node } +import v2.std.integer { integer_int_type_node } +import v2.std.model_core { AlgebraInhabitanceDecl } +import v2.std.collection { List } +import v2.test.claim.type_param_binder_frame { tpb_assemble } +import v2.std.diagnostic { Accepted, Outcome, Rejected, diagnostics_fatal_reason } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool, bool_node } +import v2.std.node { Node, Symbol } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// SUBJECT: v2.compiler.infer derives a binary algebra operator's result through ONE route -- the operator's +// signature field (v2.std.compilers.target_model canonical operation) is declared by the operand type's row in +// v2.extdeps.languages.dag dag_algebra_inhabitance_decls -- replacing the Int-only `+` arm. A derived body type is +// observed through the declared-return check: a body that derives a type contradicting the declared return +// refuses arrow_body_does_not_inhabit_declared_return, while an underived body is only an accepted, counted +// undecidable obligation. + +fn aod_reason(src: String) -> Symbol { + match tpb_assemble(src: src) { + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) + Accepted { value: tree, diagnostics: _ } => + match infer(tree: tree) { + Accepted { value: _, diagnostics: _ } => ^accepted + Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) + } + } +} + +// EACH FIXTURE PROGRAM IS ASSEMBLED AND INFERRED ONCE, by a NULLARY producer enrolled in +// v2.workflow.floor_pure_producer_share floor_cross_claim_pure_producers_warm; the claims read the decided reason. +fn aod_bool_join_declared_int_reason() -> Symbol { + aod_reason(src: "module p\n\nfn f(a: Bool, b: Bool) -> Int {\n a || b\n}\n") +} + +fn aod_int_add_declared_bool_reason() -> Symbol { + aod_reason(src: "module p\n\nfn f(a: Int, b: Int) -> Bool {\n a + b\n}\n") +} + +fn aod_bool_add_reason() -> Symbol { + aod_reason(src: "module p\n\nfn f(a: Bool, b: Bool) -> Bool {\n a + b\n}\n") +} + +fn aod_int_join_reason() -> Symbol { + aod_reason(src: "module p\n\nfn f(a: Int, b: Int) -> Int {\n a || b\n}\n") +} + +fn aod_bool_join_ok_reason() -> Symbol { + aod_reason(src: "module p\n\nfn f(a: Bool, b: Bool) -> Bool {\n a || b\n}\n") +} + +fn aod_int_add_ok_reason() -> Symbol { + aod_reason(src: "module p\n\nfn g(a: Int, b: Int) -> Int {\n a + b\n}\n") +} + +// (1) `||` OVER BOOL DERIVES BOOL: declared Int, so the derived Bool body refuses. RED ON THE BASE: no arm +// derived `||`, the body was underived, and the program was accepted with an undecidable advisory. +test fn aod_bool_join_derives_bool() -> Bool { + aod_bool_join_declared_int_reason() == ^arrow_body_does_not_inhabit_declared_return +} + +// (2) `+` OVER INT STILL DERIVES INT, now through Int's ordered-ring row: declared Bool, so it refuses. +test fn aod_int_add_still_derives_int() -> Bool { + aod_int_add_declared_bool_reason() == ^arrow_body_does_not_inhabit_declared_return +} + +// (3) NO ROW, NO DERIVATION: Bool carries no ring add, and Int no lattice join -- each refuses at the operator. +test fn aod_bool_add_refuses() -> Bool { + aod_bool_add_reason() == ^infer_transform_operand_type_mismatch +} + +test fn aod_int_join_refuses() -> Bool { + aod_int_join_reason() == ^infer_transform_operand_type_mismatch +} + +// (4) THE ACCEPTED CONTROLS: each operator over its own carrier, declared correctly, is accepted. +test fn aod_well_typed_operators_are_accepted() -> Bool { + aod_bool_join_ok_reason() == ^accepted + && aod_int_add_ok_reason() == ^accepted +} + +// (5) A ROW IS SELECTED BY THE CARRIER ITS STRUCTURE IS OVER, NEVER BY A COPY STORED BESIDE IT. These supply the +// rows at the derivation's own interface (infer_algebra_field_result_type); (1)-(4) above are the real-path +// inhabitance, running the production rows through assemble and infer. Each supplied row is a CORRELATED-FIELD +// MUTATION: its outer `inhabitant` disagrees with the ^inhabitant_edge of its own `algebra` node. RED ON THE +// PRE-FIX HEAD, which selected by the outer field: `Int || Int` derived Int from a Bool boolean-algebra. +fn aod_mismatched_row(outer: Node, algebra: Node) -> List { + [AlgebraInhabitanceDecl { algebra: algebra, inhabitant: outer, witness: outer }] +} + +fn aod_result_is_type(r: InferAlgebraFieldResult, expected: Node) -> Bool { + match r { + AlgebraFieldResultType { result: t } => t == expected + AlgebraFieldNotCarried => false + AlgebraFieldRowMalformed { cause: _ } => false + } +} + +fn aod_result_not_carried(r: InferAlgebraFieldResult) -> Bool { + match r { + AlgebraFieldResultType { result: _ } => false + AlgebraFieldNotCarried => true + AlgebraFieldRowMalformed { cause: _ } => false + } +} + +// An outer Int over a Bool boolean algebra lends Int no lattice join. +test fn aod_outer_inhabitant_lends_no_join() -> Bool { + aod_result_not_carried(r: infer_algebra_field_result_type( + rows: aod_mismatched_row(outer: integer_int_type_node(), algebra: boolean_algebra_node(inhabitant: bool_node())), + operand_type: integer_int_type_node(), + field: ^lattice_field_join + )) +} + +// The inverse: an outer Bool over an Int ordered ring lends Bool no ring add. +test fn aod_outer_inhabitant_lends_no_add() -> Bool { + aod_result_not_carried(r: infer_algebra_field_result_type( + rows: aod_mismatched_row(outer: bool_node(), algebra: ordered_ring_node(inhabitant: integer_int_type_node())), + operand_type: bool_node(), + field: ^ring_field_add + )) +} + +// The positive arm of the same mutation: the structure answers for the carrier it IS over, whatever the outer copy +// says, so the derivation cannot be passing merely by refusing every mismatched row. +test fn aod_embedded_carrier_selects_the_row() -> Bool { + aod_result_is_type( + r: infer_algebra_field_result_type( + rows: aod_mismatched_row(outer: integer_int_type_node(), algebra: boolean_algebra_node(inhabitant: bool_node())), + operand_type: bool_node(), + field: ^lattice_field_join + ), + expected: bool_node() + ) +} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 01759c655ad..edeabcd03dc 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -838,6 +838,9 @@ import v2.std.algebra { any } // tpb_assemble and inspected one Bool. The rows now read three nullary producers, one per program -- the // call-projection program's producer serving two rows -- whose values are a record of two Bools and two // Bools. WARM: one assembly is more than one claim's budget. +// THE algebra_operator_derivation PROGRAMS ARE ASSEMBLED AND INFERRED ONCE EACH: six one-function sources, +// each a whole tpb_assemble + infer, each claim reading one Symbol (the fatal reason, or ^accepted). WARM: one +// assembly is more than one claim's budget. // THE collection_callback_realization PROGRAMS ARE ASSEMBLED ONCE EACH. Each claim assembled a one-module // source through fmi_assemble (and, for two, infer) and inspected one Bool or Symbol, well over the new-witness // eval-step cap. The rows now read five nullary producers, one per program -- the map-over-records program's @@ -1492,6 +1495,12 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.value_base_projection.vbp_call_projection_reading", "v2.test.claim.value_base_projection.vbp_field_spelled_like_a_param_keeps_field", "v2.test.claim.value_base_projection.vbp_undeclared_field_is_carried", + "v2.test.claim.algebra_operator_derivation.aod_bool_join_declared_int_reason", + "v2.test.claim.algebra_operator_derivation.aod_int_add_declared_bool_reason", + "v2.test.claim.algebra_operator_derivation.aod_bool_add_reason", + "v2.test.claim.algebra_operator_derivation.aod_int_join_reason", + "v2.test.claim.algebra_operator_derivation.aod_bool_join_ok_reason", + "v2.test.claim.algebra_operator_derivation.aod_int_add_ok_reason", "v2.test.claim.compiler.collection_callback_realization.ccr_map_records_reading", "v2.test.claim.compiler.collection_callback_realization.ccr_map_undeclared_field_reason", "v2.test.claim.compiler.collection_callback_realization.ccr_piped_map_binds_its_row",