From 4f981be93966af4bfe3c14035d72001070b54eff Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 17:16:28 -0400 Subject: [PATCH 1/3] =?UTF-8?q?WIP:=20Variant-parameterization=20sweep=20r?= =?UTF-8?q?esume=20=E2=80=94=20apply=20refined=20L1.4.b=20bar=20(PR=20#34?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/compiler/00_compile.dag | 6 ++-- src/v4/compiler/02_parse.dag | 6 ++-- src/v4/compiler/03_normalize.dag | 6 ++-- src/v4/compiler/03_resolve.dag | 6 ++-- src/v4/compiler/04_infer.dag | 8 ++--- src/v4/compiler/05_emit.dag | 4 +-- src/v4/compiler/05_eval.dag | 4 +-- src/v4/compiler/06_translate.dag | 12 +++---- src/v4/compiler/self_host.dag | 12 +++---- src/v4/lens/affected_set_examples.dag | 4 +-- src/v4/lens/cost.dag | 4 +-- src/v4/std/coercion.dag | 6 ++-- src/v4/std/constraints.dag | 4 +-- src/v4/std/diagnostic.dag | 31 +++++++++++++------ src/v4/std/find_witness.dag | 10 +++--- src/v4/std/float.dag | 6 ++-- .../test/claim/algebra_laws/nat_semiring.dag | 4 +-- .../show_correct_code.dag | 16 +++++----- .../impossible_bug/idempotency_contract.dag | 6 ++-- .../nested_optional_flatten.dag | 6 ++-- .../impossible_bug/suboptimal_complexity.dag | 4 +-- .../impossible_bug/transport_type_drift.dag | 6 ++-- .../impossible_bug/unenumerated_effects.dag | 4 +-- .../unhandled_diagnostic_paths.dag | 8 ++--- .../claim/manual/diagnostic_assert_eval.dag | 6 ++-- .../test/claim/manual/eval_host_model_mvp.dag | 2 +- .../manual/infer_emit_compile_anchor.dag | 8 ++--- .../claim/manual/outcome_diagnostics_eq.dag | 6 ++-- .../manual/process_numeric_refinements.dag | 8 ++--- .../validate_then_compile_public_terminal.dag | 4 +-- .../claim/workflow/pipeline_rejections.dag | 4 +-- 31 files changed, 115 insertions(+), 106 deletions(-) diff --git a/src/v4/compiler/00_compile.dag b/src/v4/compiler/00_compile.dag index 232d28c159b..04a6cd4df34 100644 --- a/src/v4/compiler/00_compile.dag +++ b/src/v4/compiler/00_compile.dag @@ -27,7 +27,7 @@ import v4.std.diagnostic { ExternalContractUnknown, Locus, Outcome, - PortLocus, + port_locus, Rejected, Unavailable, bind_outcome, @@ -217,7 +217,7 @@ fn compile_inferred( Eval { host_interp: _ } => outcome_rejected( compile_eval_not_realized_diagnostic( - at: PortLocus { port: compile_stage_locus_port } + at: port_locus(port: compile_stage_locus_port) ) ) } @@ -290,7 +290,7 @@ fn compile_ingest_staging(source: Source, target: TargetModel) -> Outcome Node { fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { - let at = PortLocus { - port: parse_stage_locus_port - } + let at = port_locus(port: parse_stage_locus_port) let ntok = count(tokens.tokens) let grammar_node = grammar_to_node(grammar: grammar) if !well_formed(n: grammar_node) { diff --git a/src/v4/compiler/03_normalize.dag b/src/v4/compiler/03_normalize.dag index 51b2f67af9b..82fb3bd5dbd 100644 --- a/src/v4/compiler/03_normalize.dag +++ b/src/v4/compiler/03_normalize.dag @@ -18,7 +18,7 @@ import v4.extdeps.languages.dag { } import v4.std.diagnostic { Diagnostic, - NodeLocus, + node_locus, Outcome, UserInputBoundary, Accepted, @@ -93,7 +93,7 @@ fn classify_sugar(n: Node) -> SurfaceSugarKind? { fn malformed_sugar_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: normalize_reason_malformed_sugar, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: UserInputBoundary } } } @@ -102,7 +102,7 @@ fn malformed_sugar_diagnostic(n: Node) -> Diagnostic { fn post_normalize_not_well_formed_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: normalize_reason_post_normalize_not_well_formed, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: UserInputBoundary } } } diff --git a/src/v4/compiler/03_resolve.dag b/src/v4/compiler/03_resolve.dag index a1d8e3aeae7..866312a3626 100644 --- a/src/v4/compiler/03_resolve.dag +++ b/src/v4/compiler/03_resolve.dag @@ -17,7 +17,7 @@ import v4.extdeps.languages.dag { import v4.std.collection { Set } import v4.std.diagnostic { Diagnostic, - NodeLocus, + node_locus, Outcome, UserInputBoundary, Accepted, @@ -217,7 +217,7 @@ fn lookup_chain(s: Scope, name: Symbol) -> Symbol? { fn malformed_tree_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: resolve_reason_malformed_tree, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: UserInputBoundary } } } @@ -226,7 +226,7 @@ fn malformed_tree_diagnostic(n: Node) -> Diagnostic { fn unbound_symbol_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: resolve_reason_unbound_symbol, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: UserInputBoundary } } } diff --git a/src/v4/compiler/04_infer.dag b/src/v4/compiler/04_infer.dag index 7957b5ad0e8..4795efa9e12 100644 --- a/src/v4/compiler/04_infer.dag +++ b/src/v4/compiler/04_infer.dag @@ -24,7 +24,7 @@ import v4.std.constraints { import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, Unavailable, Accepted, @@ -106,14 +106,14 @@ data infer_canonical_grounding_incoherent: Symbol = infer_canonical_grounding_in fn infer_facts_lookup_miss_diagnostic(key: Node) -> Diagnostic { Diagnostic { reason: infer_facts_lookup_miss, - at: NodeLocus { node: key }, + at: node_locus(node: key), correction: Unavailable { reason: ExternalContractUnknown } } } fn infer_canonical_grounding_incoherent_diagnostic(node: Node) -> Diagnostic { Diagnostic { reason: infer_canonical_grounding_incoherent, - at: NodeLocus { node: node }, + at: node_locus(node: node), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -122,7 +122,7 @@ fn infer_canonical_grounding_incoherent_diagnostic(node: Node) -> Diagnostic { fn infer_descent_not_derived_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: infer_descent_not_derived, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/compiler/05_emit.dag b/src/v4/compiler/05_emit.dag index c12c3dd8f31..a6c07a466c1 100644 --- a/src/v4/compiler/05_emit.dag +++ b/src/v4/compiler/05_emit.dag @@ -29,7 +29,7 @@ import v4.std.diagnostic { Accepted, Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, Rejected, Unavailable, @@ -43,7 +43,7 @@ data emit_serialize_emitted_mismatch: Symbol = emit_serialize_emitted_mismatch fn emit_serialize_emitted_mismatch_diagnostic(emitted: Node, target: TargetModel) -> Diagnostic { Diagnostic { reason: emit_serialize_emitted_mismatch, - at: NodeLocus { node: emitted }, + at: node_locus(node: emitted), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/compiler/05_eval.dag b/src/v4/compiler/05_eval.dag index e2bb761426d..1b14d0c5f1a 100644 --- a/src/v4/compiler/05_eval.dag +++ b/src/v4/compiler/05_eval.dag @@ -52,7 +52,7 @@ import v4.std.diagnostic { Correction, Diagnostic, NoCorrectionReason, - NodeLocus, + node_locus, Outcome, Unavailable, Accepted, @@ -182,7 +182,7 @@ data eval_rejected_canonical_mismatch: Symbol = eval_rejected_canonical_mismatch fn eval_diagnostic(reason: Symbol, node: Node) -> Diagnostic { Diagnostic { reason: reason, - at: NodeLocus { node: node }, + at: node_locus(node: node), correction: Unavailable { reason: AmbiguousIntent } } } diff --git a/src/v4/compiler/06_translate.dag b/src/v4/compiler/06_translate.dag index c75a9f6df68..6372689209d 100644 --- a/src/v4/compiler/06_translate.dag +++ b/src/v4/compiler/06_translate.dag @@ -33,9 +33,9 @@ import v4.std.diagnostic { Accepted, Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, - PortLocus, + port_locus, Rejected, Unavailable, bind_outcome, @@ -78,7 +78,7 @@ data translate_child_reattachment_not_realized: Symbol = translate_child_reattac fn translate_target_bundle_malformed_diagnostic(target: TargetModel) -> Diagnostic { Diagnostic { reason: translate_target_bundle_malformed, - at: NodeLocus { node: target }, + at: node_locus(node: target), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -88,7 +88,7 @@ fn translate_target_bundle_duplicate_edge_diagnostic( ) -> Diagnostic { Diagnostic { reason: translate_target_bundle_duplicate_edge, - at: NodeLocus { node: target }, + at: node_locus(node: target), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -125,14 +125,14 @@ fn target_bundle_child_lookup_step( fn translate_target_source_not_realized_diagnostic() -> Diagnostic { Diagnostic { reason: translate_target_source_not_realized, - at: PortLocus { port: translate_stage_locus_port }, + at: port_locus(port: translate_stage_locus_port), correction: Unavailable { reason: ExternalContractUnknown } } } fn translate_child_reattachment_not_realized_diagnostic(parent: Node) -> Diagnostic { Diagnostic { reason: translate_child_reattachment_not_realized, - at: NodeLocus { node: parent }, + at: node_locus(node: parent), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/compiler/self_host.dag b/src/v4/compiler/self_host.dag index 3756c570a58..0ae9edc63da 100644 --- a/src/v4/compiler/self_host.dag +++ b/src/v4/compiler/self_host.dag @@ -10,9 +10,9 @@ import v4.std.collection { List } import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, - PortLocus, + port_locus, Rejected, Unavailable, diagnostics_singleton @@ -76,7 +76,7 @@ data fixed_point_not_realized: Symbol = fixed_point_not_realized fn self_host_runner_not_realized_diagnostic() -> Diagnostic { Diagnostic { reason: self_host_runner_not_realized, - at: PortLocus { port: self_host_runner_port }, + at: port_locus(port: self_host_runner_port), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -106,7 +106,7 @@ fn bootstrap_roundtrip_scaffold( Violates { diagnostic: Diagnostic { reason: bootstrap_roundtrip_not_realized, - at: NodeLocus { node: expected_stage }, + at: node_locus(node: expected_stage), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -120,7 +120,7 @@ fn fixed_point_scaffold( Violates { diagnostic: Diagnostic { reason: fixed_point_not_realized, - at: NodeLocus { node: reference_stage }, + at: node_locus(node: reference_stage), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -134,7 +134,7 @@ fn stage_emission_equality_scaffold( Violates { diagnostic: Diagnostic { reason: stage_emission_equality_not_realized, - at: NodeLocus { node: reference_stage1 }, + at: node_locus(node: reference_stage1), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/lens/affected_set_examples.dag b/src/v4/lens/affected_set_examples.dag index a0eee16d1c3..11b4ee3e87c 100644 --- a/src/v4/lens/affected_set_examples.dag +++ b/src/v4/lens/affected_set_examples.dag @@ -8,7 +8,7 @@ module v4.lens.affected_set_examples import v4.std.diagnostic { Diagnostic, - NodeLocus, + node_locus, Unavailable, ExternalContractUnknown, diagnostics_singleton @@ -52,7 +52,7 @@ data affected_set_example_edit: Edit = Edit { data affected_set_example_invalid_edit_diagnostic: Diagnostic = Diagnostic { reason: affected_set_example_reason, - at: NodeLocus { node: affected_set_example_node }, + at: node_locus(node: affected_set_example_node), correction: Unavailable { reason: ExternalContractUnknown } } diff --git a/src/v4/lens/cost.dag b/src/v4/lens/cost.dag index c63171569c3..889ad69edd2 100644 --- a/src/v4/lens/cost.dag +++ b/src/v4/lens/cost.dag @@ -47,7 +47,7 @@ import v4.std.cardinality { NonZeroNat } import v4.std.diagnostic { AmbiguousIntent, Diagnostic, - NodeLocus, + node_locus, Unavailable } import v4.std.node { @@ -176,7 +176,7 @@ fn unknown_cost(reason: String) -> SymbolicCost { fn symbolic_cost_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: cost_reason_unmodeled_symbolic_cost, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: AmbiguousIntent } } } diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag index 1ee28ca2e14..0e0b8f11a66 100644 --- a/src/v4/std/coercion.dag +++ b/src/v4/std/coercion.dag @@ -17,7 +17,7 @@ import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, None, - NodeLocus, + node_locus, Outcome, Rejected, Unavailable, @@ -82,7 +82,7 @@ fn coercion_not_realized_diagnostic( ) -> Diagnostic { Diagnostic { reason: coercion_mismatch_reason(kind: kind), - at: NodeLocus { node: source.node }, + at: node_locus(node: source.node), correction: Unavailable { reason: ExternalContractUnknown } } } @@ -116,7 +116,7 @@ fn declared_inhabitant_candidates(inhabitants_root: Node) -> List { fn coercion_candidate_set_not_closed_diagnostic(inhabitants_root: Node) -> Diagnostic { Diagnostic { reason: coercion_mismatch_candidate_set_not_closed, - at: NodeLocus { node: inhabitants_root }, + at: node_locus(node: inhabitants_root), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/std/constraints.dag b/src/v4/std/constraints.dag index d89d4b57250..9609f44d153 100644 --- a/src/v4/std/constraints.dag +++ b/src/v4/std/constraints.dag @@ -14,7 +14,7 @@ import v4.std.diagnostic { Accepted, Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, Rejected, Unavailable, @@ -61,7 +61,7 @@ type CanonicalGroundingWitness { fn constraints_not_realized_diagnostic(graph: ConstraintGraph) -> Diagnostic { Diagnostic { reason: constraints_not_realized, - at: NodeLocus { node: graph.root }, + at: node_locus(node: graph.root), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/std/diagnostic.dag b/src/v4/std/diagnostic.dag index 9391a79110a..510c9d34457 100644 --- a/src/v4/std/diagnostic.dag +++ b/src/v4/std/diagnostic.dag @@ -18,11 +18,16 @@ import v4.std.node { Node } type Extent = WholeFile | ByteRange { start: Int, end: Int } +// 🟢 coproduct dissolution — L1.4.b Pattern B: Node/Port payload tags +// are recoverable from the parameterized anchor type. +type LocusAnchor { + at: T +} // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. type Locus = Textual { file: Symbol, extent: Extent } - | NodeLocus { node: Node } - | PortLocus { port: Symbol } + | NodeLocus { anchor: LocusAnchor } + | PortLocus { anchor: LocusAnchor } // 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. type NoCorrectionReason = UserInputBoundary @@ -59,6 +64,12 @@ type StageDiagnosticPolicy { fn diagnostics_singleton(d: Diagnostic) -> NonEmptyDiagnostics { NonEmptyDiagnostics { head: d, tail: [] } } +fn node_locus(node: Node) -> Locus { + NodeLocus { anchor: LocusAnchor { at: node } } +} +fn port_locus(port: Symbol) -> Locus { + PortLocus { anchor: LocusAnchor { at: port } } +} fn outcome_accepted(value: T) -> Outcome { Accepted { value: value, diagnostics: None } } @@ -81,18 +92,18 @@ fn locus_eq(a: Locus, b: Locus) -> Bool { match a { Textual { file: fa, extent: ea } => match b { Textual { file: fb, extent: eb } => (fa == fb) && eq(a: ea, b: eb) - NodeLocus { node: _ } => false - PortLocus { port: _ } => false + NodeLocus { anchor: _ } => false + PortLocus { anchor: _ } => false } - NodeLocus { node: na } => match b { + NodeLocus { anchor: na } => match b { Textual { file: _, extent: _ } => false - NodeLocus { node: nb } => na == nb - PortLocus { port: _ } => false + NodeLocus { anchor: nb } => na.at == nb.at + PortLocus { anchor: _ } => false } - PortLocus { port: pa } => match b { + PortLocus { anchor: pa } => match b { Textual { file: _, extent: _ } => false - NodeLocus { node: _ } => false - PortLocus { port: pb } => pa == pb + NodeLocus { anchor: _ } => false + PortLocus { anchor: pb } => pa.at == pb.at } } } diff --git a/src/v4/std/find_witness.dag b/src/v4/std/find_witness.dag index bec6320feda..91976fb6798 100644 --- a/src/v4/std/find_witness.dag +++ b/src/v4/std/find_witness.dag @@ -16,7 +16,7 @@ import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, None, - NodeLocus, + node_locus, Outcome, Rejected, Unavailable, @@ -59,28 +59,28 @@ type MultiplicityPolicy fn find_witness_no_candidate_diagnostic(source_facts: Node) -> Diagnostic { Diagnostic { reason: find_witness_reason_no_candidate, - at: NodeLocus { node: source_facts }, + at: node_locus(node: source_facts), correction: Unavailable { reason: ExternalContractUnknown } } } fn find_witness_ambiguous_candidate_diagnostic(source_facts: Node) -> Diagnostic { Diagnostic { reason: find_witness_reason_ambiguous_candidate, - at: NodeLocus { node: source_facts }, + at: node_locus(node: source_facts), correction: Unavailable { reason: ExternalContractUnknown } } } fn find_witness_not_realized_diagnostic(source_facts: Node) -> Diagnostic { Diagnostic { reason: find_witness_reason_not_realized, - at: NodeLocus { node: source_facts }, + at: node_locus(node: source_facts), correction: Unavailable { reason: ExternalContractUnknown } } } fn find_witness_invalid_witness_diagnostic(source_facts: Node) -> Diagnostic { Diagnostic { reason: find_witness_reason_invalid_witness, - at: NodeLocus { node: source_facts }, + at: node_locus(node: source_facts), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/std/float.dag b/src/v4/std/float.dag index b9df9f1ce6e..88688961c1d 100644 --- a/src/v4/std/float.dag +++ b/src/v4/std/float.dag @@ -1,7 +1,7 @@ // src/v4/std/float.dag // Scope: IEEE-754 Float32/Float64 interchange, specials, body carriers, and ordered compare semantics. // Owns: Float32Interchange, Float64Interchange, FloatSpecial, FloatBody, Float32, Float64, Float, float_totalizer_reason_ieee754_nan_unordered, float_totalizer_port_ieee754_nan_totalizer, sign_rank_lex, ordering_invert, float_finite_unsigned_field_order, float_special_rank, float_body_is_nan, float_finite_magnitude_zero, float_body_compare_semantic_total, float_body_compare_ieee_ordered_outcome, float_ordered_compare_nan_rejected, float_ieee_ordered_compare_outcome, float_ordered_compare_tier2 -// Consumes: std/node.dag (Symbol); std/machine.dag (Bit, Word32, Word64); std/algebra.dag (Ordering, Less, Equal, Greater); std/diagnostic.dag (Diagnostic, Outcome, PortLocus, Produced, Rejected, Unavailable, UserInputBoundary); std/logic.dag (Bool); std/nat.dag (Nat, is_zero, nat_compare). +// Consumes: std/node.dag (Symbol); std/machine.dag (Bit, Word32, Word64); std/algebra.dag (Ordering, Less, Equal, Greater); std/diagnostic.dag (Diagnostic, Outcome, port_locus, Produced, Rejected, Unavailable, UserInputBoundary); std/logic.dag (Bool); std/nat.dag (Nat, is_zero, nat_compare). // Status: std float vocabulary (32/64, specials, IEEE-ordered compare). // Anchor: https://en.wikipedia.org/wiki/IEEE_754 // Ledger: CP-3229-GREEN-TERMINAL, SL-3229-FLOAT-NOMINAL. @@ -11,7 +11,7 @@ module v4.std.float import v4.std.algebra { Ordering, Less, Equal, Greater } -import v4.std.diagnostic {Diagnostic, Outcome, PortLocus, Unavailable, UserInputBoundary, Accepted, None, diagnostics_singleton} +import v4.std.diagnostic {Diagnostic, Outcome, port_locus, Unavailable, UserInputBoundary, Accepted, None, diagnostics_singleton} import v4.std.logic { Bool } import v4.std.machine { Bit, Word32, Word64 } import v4.std.nat { Nat, nat_compare, is_zero } @@ -164,7 +164,7 @@ fn float_body_compare_ieee_ordered_outcome(a: FloatBody, b: FloatBody) -> Outcom fn float_ordered_compare_nan_rejected() -> Outcome { Rejected { diagnostics: diagnostics_singleton(d: Diagnostic { reason: float_totalizer_reason_ieee754_nan_unordered, - at: PortLocus { port: float_totalizer_port_ieee754_nan_totalizer }, + at: port_locus(port: float_totalizer_port_ieee754_nan_totalizer), correction: Unavailable { reason: UserInputBoundary }, }) } } diff --git a/src/v4/test/claim/algebra_laws/nat_semiring.dag b/src/v4/test/claim/algebra_laws/nat_semiring.dag index 47b8af2eeec..03e6e223b15 100644 --- a/src/v4/test/claim/algebra_laws/nat_semiring.dag +++ b/src/v4/test/claim/algebra_laws/nat_semiring.dag @@ -12,7 +12,7 @@ module v4.test.claim.algebra_laws.nat_semiring import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -160,7 +160,7 @@ data claim_nat_add_wrong_identity_falsifies_law: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: algebra_law_violation_reason, - at: NodeLocus { node: falsification_nat_add_wrong_identity }, + at: node_locus(node: falsification_nat_add_wrong_identity), correction: Suggested { node: nat_add_left_identity_input } } ), diff --git a/src/v4/test/claim/diagnostic_correction/show_correct_code.dag b/src/v4/test/claim/diagnostic_correction/show_correct_code.dag index 5f31dd00486..95494f40afe 100644 --- a/src/v4/test/claim/diagnostic_correction/show_correct_code.dag +++ b/src/v4/test/claim/diagnostic_correction/show_correct_code.dag @@ -14,9 +14,9 @@ import v4.std.diagnostic { ByteRange, Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, - PortLocus, + port_locus, Rejected, Suggested, Textual, @@ -117,7 +117,7 @@ data claim_complexity_diagnostic_suggests_correct_code: TestClaim = DiagnosticCl expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_complexity_reason, - at: NodeLocus { node: falsification_complexity_diagnostic_without_correct_code }, + at: node_locus(node: falsification_complexity_diagnostic_without_correct_code), correction: Suggested { node: complexity_correction_expected_node } } ), @@ -132,7 +132,7 @@ data claim_transport_diagnostic_suggests_shared_contract: TestClaim = Diagnostic expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_transport_reason, - at: NodeLocus { node: falsification_transport_diagnostic_without_correct_code }, + at: node_locus(node: falsification_transport_diagnostic_without_correct_code), correction: Suggested { node: transport_correction_expected_node } } ), @@ -147,7 +147,7 @@ data claim_ambiguous_boundary_diagnostic_names_no_correction_reason: TestClaim = expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_ambiguous_boundary_reason, - at: NodeLocus { node: falsification_ambiguous_boundary_without_unavailable_reason }, + at: node_locus(node: falsification_ambiguous_boundary_without_unavailable_reason), correction: Unavailable { reason: AmbiguousIntent } } ), @@ -192,7 +192,7 @@ data claim_port_diagnostic_carries_port_locus: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_port_reason, - at: PortLocus { port: correction_port_symbol }, + at: port_locus(port: correction_port_symbol), correction: Suggested { node: transport_correction_expected_node } } ), @@ -207,7 +207,7 @@ data claim_external_contract_diagnostic_names_no_correction_reason: TestClaim = expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_external_contract_reason, - at: NodeLocus { node: falsification_external_contract_without_reason }, + at: node_locus(node: falsification_external_contract_without_reason), correction: Unavailable { reason: ExternalContractUnknown } } ), @@ -222,7 +222,7 @@ data claim_user_boundary_diagnostic_names_no_correction_reason: TestClaim = Diag expected_rejection: diagnostics_singleton( d: Diagnostic { reason: correction_user_boundary_reason, - at: NodeLocus { node: falsification_user_boundary_without_reason }, + at: node_locus(node: falsification_user_boundary_without_reason), correction: Unavailable { reason: UserInputBoundary } } ), diff --git a/src/v4/test/claim/impossible_bug/idempotency_contract.dag b/src/v4/test/claim/impossible_bug/idempotency_contract.dag index c4f585942ce..18213ce61da 100644 --- a/src/v4/test/claim/impossible_bug/idempotency_contract.dag +++ b/src/v4/test/claim/impossible_bug/idempotency_contract.dag @@ -38,7 +38,7 @@ module v4.test.claim.impossible_bug.idempotency_contract import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -109,7 +109,7 @@ data claim_repeated_append_in_idempotent_position_caught: TestClaim = Diagnostic expected_rejection: diagnostics_singleton( d: Diagnostic { reason: idempotency_repetition_reason, - at: NodeLocus { node: falsification_repeated_append_in_idempotent_position }, + at: node_locus(node: falsification_repeated_append_in_idempotent_position), correction: Suggested { node: idempotent_inhabitant_input } } ), @@ -124,7 +124,7 @@ data claim_nonidempotent_in_idempotent_position_caught: TestClaim = DiagnosticCl expected_rejection: diagnostics_singleton( d: Diagnostic { reason: idempotency_violation_reason, - at: NodeLocus { node: falsification_nonidempotent_in_idempotent_position }, + at: node_locus(node: falsification_nonidempotent_in_idempotent_position), correction: Suggested { node: idempotent_inhabitant_input } } ), diff --git a/src/v4/test/claim/impossible_bug/nested_optional_flatten.dag b/src/v4/test/claim/impossible_bug/nested_optional_flatten.dag index 7d42273f9e3..4060819a297 100644 --- a/src/v4/test/claim/impossible_bug/nested_optional_flatten.dag +++ b/src/v4/test/claim/impossible_bug/nested_optional_flatten.dag @@ -24,7 +24,7 @@ module v4.test.claim.impossible_bug.nested_optional_flatten import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -101,7 +101,7 @@ data claim_optional_double_unwrap_rejected: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: double_unwrap_reason, - at: NodeLocus { node: falsification_optional_double_unwrap }, + at: node_locus(node: falsification_optional_double_unwrap), correction: Suggested { node: flattened_optional_input } } ), @@ -116,7 +116,7 @@ data claim_nested_optional_collapses: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: nested_optional_reason, - at: NodeLocus { node: falsification_nested_optional }, + at: node_locus(node: falsification_nested_optional), correction: Suggested { node: flattened_optional_input } } ), diff --git a/src/v4/test/claim/impossible_bug/suboptimal_complexity.dag b/src/v4/test/claim/impossible_bug/suboptimal_complexity.dag index 97e1a5bde32..65816adbea4 100644 --- a/src/v4/test/claim/impossible_bug/suboptimal_complexity.dag +++ b/src/v4/test/claim/impossible_bug/suboptimal_complexity.dag @@ -42,7 +42,7 @@ module v4.test.claim.impossible_bug.suboptimal_complexity import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, NonEmptyDiagnostics, None, Outcome, @@ -93,7 +93,7 @@ fn expected_complexity_rejection(input: Node, reason: Symbol, correction: Node) diagnostics_singleton( d: Diagnostic { reason: reason, - at: NodeLocus { node: input }, + at: node_locus(node: input), correction: Suggested { node: correction } } ) diff --git a/src/v4/test/claim/impossible_bug/transport_type_drift.dag b/src/v4/test/claim/impossible_bug/transport_type_drift.dag index d37a8f7ac81..f4202e3b1ab 100644 --- a/src/v4/test/claim/impossible_bug/transport_type_drift.dag +++ b/src/v4/test/claim/impossible_bug/transport_type_drift.dag @@ -24,7 +24,7 @@ module v4.test.claim.impossible_bug.transport_type_drift import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -103,7 +103,7 @@ data claim_target_contract_drift_impossible: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: target_transport_drift_reason, - at: NodeLocus { node: falsification_target_contract_drift }, + at: node_locus(node: falsification_target_contract_drift), correction: Suggested { node: shared_wire_contract_input } } ), @@ -118,7 +118,7 @@ data claim_wire_contract_drift_impossible: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: transport_drift_reason, - at: NodeLocus { node: falsification_wire_contract_drift }, + at: node_locus(node: falsification_wire_contract_drift), correction: Suggested { node: shared_wire_contract_input } } ), diff --git a/src/v4/test/claim/impossible_bug/unenumerated_effects.dag b/src/v4/test/claim/impossible_bug/unenumerated_effects.dag index 6d145bb8051..8ddf833d9e2 100644 --- a/src/v4/test/claim/impossible_bug/unenumerated_effects.dag +++ b/src/v4/test/claim/impossible_bug/unenumerated_effects.dag @@ -27,7 +27,7 @@ module v4.test.claim.impossible_bug.unenumerated_effects import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -125,7 +125,7 @@ data claim_redundant_read_caught: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: redundant_read_reason, - at: NodeLocus { node: falsification_redundant_read }, + at: node_locus(node: falsification_redundant_read), correction: Suggested { node: explicit_reread_input } } ), diff --git a/src/v4/test/claim/impossible_bug/unhandled_diagnostic_paths.dag b/src/v4/test/claim/impossible_bug/unhandled_diagnostic_paths.dag index f8a62c4378c..99640fa5041 100644 --- a/src/v4/test/claim/impossible_bug/unhandled_diagnostic_paths.dag +++ b/src/v4/test/claim/impossible_bug/unhandled_diagnostic_paths.dag @@ -26,7 +26,7 @@ module v4.test.claim.impossible_bug.unhandled_diagnostic_paths import v4.std.diagnostic { Accepted, Diagnostic, - NodeLocus, + node_locus, None, Outcome, Rejected, @@ -121,7 +121,7 @@ data claim_unproven_division_rejected: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: unhandled_division_reason, - at: NodeLocus { node: falsification_division_by_zero_unhandled }, + at: node_locus(node: falsification_division_by_zero_unhandled), correction: Suggested { node: total_division_input } } ), @@ -136,7 +136,7 @@ data claim_unproven_oob_index_rejected: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: unhandled_index_reason, - at: NodeLocus { node: falsification_oob_index_unhandled }, + at: node_locus(node: falsification_oob_index_unhandled), correction: Suggested { node: checked_index_input } } ), @@ -151,7 +151,7 @@ data claim_force_unwrap_count_zero: TestClaim = DiagnosticClaim { expected_rejection: diagnostics_singleton( d: Diagnostic { reason: force_unwrap_reason, - at: NodeLocus { node: falsification_force_unwrap_survives }, + at: node_locus(node: falsification_force_unwrap_survives), correction: Suggested { node: total_unwrap_input } } ), diff --git a/src/v4/test/claim/manual/diagnostic_assert_eval.dag b/src/v4/test/claim/manual/diagnostic_assert_eval.dag index 2cd3b5b90ec..8f063435f69 100644 --- a/src/v4/test/claim/manual/diagnostic_assert_eval.dag +++ b/src/v4/test/claim/manual/diagnostic_assert_eval.dag @@ -20,7 +20,7 @@ import v4.compiler.eval { import v4.std.diagnostic { AmbiguousIntent, Diagnostic, - NodeLocus, + node_locus, NonEmptyDiagnostics, Outcome, Accepted, @@ -55,7 +55,7 @@ fn diag_assert_node() -> Node { fn diag_assert_d() -> Diagnostic { Diagnostic { reason: diag_assert_reason, - at: NodeLocus { node: diag_assert_node() }, + at: node_locus(node: diag_assert_node()), correction: Unavailable { reason: AmbiguousIntent } } } @@ -64,7 +64,7 @@ fn diag_assert_d() -> Diagnostic { fn diag_assert_other_d() -> Diagnostic { Diagnostic { reason: diag_assert_other, - at: NodeLocus { node: diag_assert_node() }, + at: node_locus(node: diag_assert_node()), correction: Unavailable { reason: AmbiguousIntent } } } diff --git a/src/v4/test/claim/manual/eval_host_model_mvp.dag b/src/v4/test/claim/manual/eval_host_model_mvp.dag index 40b17763694..5b1674e7ec1 100644 --- a/src/v4/test/claim/manual/eval_host_model_mvp.dag +++ b/src/v4/test/claim/manual/eval_host_model_mvp.dag @@ -28,7 +28,7 @@ import v4.std.diagnostic { Accepted, Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, None, Outcome, Rejected, diff --git a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag index ede13f686ee..a40011a7f62 100644 --- a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag +++ b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag @@ -23,9 +23,9 @@ import v4.std.collection { Map } import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, - PortLocus, + port_locus, Unavailable } import v4.std.node { Conj, Node, Symbol, TypeNode } @@ -78,7 +78,7 @@ data anchor_stub_inferred_facts: InferredFacts = InferredFacts { descent: Violates { diagnostic: Diagnostic { reason: anchor_stub_descent_not_derived, - at: NodeLocus { node: anchor_stub_empty_conj }, + at: node_locus(node: anchor_stub_empty_conj), correction: Unavailable { reason: ExternalContractUnknown } } }, @@ -91,7 +91,7 @@ data anchor_stub_empty_facts_map: Map = Map { Violates { diagnostic: Diagnostic { reason: anchor_facts_map_lookup_not_realized, - at: PortLocus { port: anchor_facts_map_lookup_not_realized }, + at: port_locus(port: anchor_facts_map_lookup_not_realized), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/test/claim/manual/outcome_diagnostics_eq.dag b/src/v4/test/claim/manual/outcome_diagnostics_eq.dag index 1f4b68918ff..112c7ceda8a 100644 --- a/src/v4/test/claim/manual/outcome_diagnostics_eq.dag +++ b/src/v4/test/claim/manual/outcome_diagnostics_eq.dag @@ -10,7 +10,7 @@ module v4.test.claim.manual.outcome_diagnostics_eq import v4.std.diagnostic { Diagnostic, - NodeLocus, + node_locus, Unavailable, ExternalContractUnknown, NonEmptyDiagnostics, @@ -34,14 +34,14 @@ data diag_eq_reason_y: Symbol = diag_eq_reason_y fn diag_eq_x() -> Diagnostic { Diagnostic { reason: diag_eq_reason_x, - at: NodeLocus { node: stub_empty_conj }, + at: node_locus(node: stub_empty_conj), correction: Unavailable { reason: ExternalContractUnknown } } } fn diag_eq_y() -> Diagnostic { Diagnostic { reason: diag_eq_reason_y, - at: NodeLocus { node: stub_empty_conj }, + at: node_locus(node: stub_empty_conj), correction: Unavailable { reason: ExternalContractUnknown } } } diff --git a/src/v4/test/claim/manual/process_numeric_refinements.dag b/src/v4/test/claim/manual/process_numeric_refinements.dag index 0739f9b9f09..8ce00e3fa22 100644 --- a/src/v4/test/claim/manual/process_numeric_refinements.dag +++ b/src/v4/test/claim/manual/process_numeric_refinements.dag @@ -19,7 +19,7 @@ import v4.extdeps.process { import v4.std.diagnostic { Accepted, Rejected, - NodeLocus + node_locus } import v4.std.node { Node } import v4.std.verification { @@ -37,21 +37,21 @@ import v4.test.claim.manual.connective_anchors { fn witness_exit_code_256_rejects() -> Bool { - match make_exit_code(value: 256, at: NodeLocus { node: stub_empty_conj }) { + match make_exit_code(value: 256, at: node_locus(node: stub_empty_conj)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics } => diagnostics.head.reason == exit_code_out_of_range } } fn witness_process_id_zero_rejects() -> Bool { - match make_process_id(value: 0, at: NodeLocus { node: stub_empty_conj }) { + match make_process_id(value: 0, at: node_locus(node: stub_empty_conj)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics } => diagnostics.head.reason == process_id_out_of_range } } fn witness_signal_num_zero_rejects() -> Bool { - match make_signal_num(value: 0, at: NodeLocus { node: stub_empty_conj }) { + match make_signal_num(value: 0, at: node_locus(node: stub_empty_conj)) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics } => diagnostics.head.reason == signal_num_out_of_range } diff --git a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag index cc8abb31bae..c8c1fa4b35c 100644 --- a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag +++ b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag @@ -30,7 +30,7 @@ import v4.std.diagnostic { Accepted, None, Outcome, - PortLocus, + port_locus, Rejected, outcome_accepted, outcome_rejected @@ -72,7 +72,7 @@ fn claim_symbol_node(s: Symbol) -> Node { fn always_reject_lens_gate(_tree: InferredTree) -> Outcome> { outcome_rejected( compile_lens_gate_rejected_diagnostic( - at: PortLocus { port: rejecting_lens_gate_at } + at: port_locus(port: rejecting_lens_gate_at) ) ) } diff --git a/src/v4/test/claim/workflow/pipeline_rejections.dag b/src/v4/test/claim/workflow/pipeline_rejections.dag index 7e00e6e9295..399b9ad4e61 100644 --- a/src/v4/test/claim/workflow/pipeline_rejections.dag +++ b/src/v4/test/claim/workflow/pipeline_rejections.dag @@ -38,7 +38,7 @@ import v4.std.node { import v4.std.diagnostic { Diagnostic, ExternalContractUnknown, - NodeLocus, + node_locus, Outcome, Accepted, None, @@ -187,7 +187,7 @@ fn workflow_inferred_facts() -> InferredFacts { descent: Violates { diagnostic: Diagnostic { reason: inferred_descent_not_derived, - at: NodeLocus { node: resolved }, + at: node_locus(node: resolved), correction: Unavailable { reason: ExternalContractUnknown } } }, From e759c559ec30f6fc57781c0af76d142c91155658 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 17:25:23 -0400 Subject: [PATCH 2/3] =?UTF-8?q?WIP:=20Variant-parameterization=20sweep=20r?= =?UTF-8?q?esume=20=E2=80=94=20apply=20refined=20L1.4.b=20bar=20(PR=20#34?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/v4/test/claim/manual/eval_host_model_mvp.dag | 1 - 1 file changed, 1 deletion(-) diff --git a/src/v4/test/claim/manual/eval_host_model_mvp.dag b/src/v4/test/claim/manual/eval_host_model_mvp.dag index 5b1674e7ec1..a0e1afa4505 100644 --- a/src/v4/test/claim/manual/eval_host_model_mvp.dag +++ b/src/v4/test/claim/manual/eval_host_model_mvp.dag @@ -28,7 +28,6 @@ import v4.std.diagnostic { Accepted, Diagnostic, ExternalContractUnknown, - node_locus, None, Outcome, Rejected, From 663fda581b057a0542800984569a422a1045e9a4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 21 May 2026 21:26:26 +0000 Subject: [PATCH 3/3] Refresh v4 float deprose header --- src/v4/std/float.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v4/std/float.dag b/src/v4/std/float.dag index 88688961c1d..29737100875 100644 --- a/src/v4/std/float.dag +++ b/src/v4/std/float.dag @@ -1,7 +1,7 @@ // src/v4/std/float.dag // Scope: IEEE-754 Float32/Float64 interchange, specials, body carriers, and ordered compare semantics. // Owns: Float32Interchange, Float64Interchange, FloatSpecial, FloatBody, Float32, Float64, Float, float_totalizer_reason_ieee754_nan_unordered, float_totalizer_port_ieee754_nan_totalizer, sign_rank_lex, ordering_invert, float_finite_unsigned_field_order, float_special_rank, float_body_is_nan, float_finite_magnitude_zero, float_body_compare_semantic_total, float_body_compare_ieee_ordered_outcome, float_ordered_compare_nan_rejected, float_ieee_ordered_compare_outcome, float_ordered_compare_tier2 -// Consumes: std/node.dag (Symbol); std/machine.dag (Bit, Word32, Word64); std/algebra.dag (Ordering, Less, Equal, Greater); std/diagnostic.dag (Diagnostic, Outcome, port_locus, Produced, Rejected, Unavailable, UserInputBoundary); std/logic.dag (Bool); std/nat.dag (Nat, is_zero, nat_compare). +// Consumes: std/node.dag (Symbol); std/machine.dag (Bit, Word32, Word64); std/algebra.dag (Ordering, Less, Equal, Greater); std/diagnostic.dag (Diagnostic, Outcome, PortLocus, Produced, Rejected, Unavailable, UserInputBoundary); std/logic.dag (Bool); std/nat.dag (Nat, is_zero, nat_compare). // Status: std float vocabulary (32/64, specials, IEEE-ordered compare). // Anchor: https://en.wikipedia.org/wiki/IEEE_754 // Ledger: CP-3229-GREEN-TERMINAL, SL-3229-FLOAT-NOMINAL.