From e6390b675591a5b18de98040fd972596f323405a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 1 Oct 2026 03:53:56 +0000 Subject: [PATCH] v2: a parameter may refine its type with a where clause; it parses and the fn refuses at the clause (body_lowering_reason_parameter_refinement_unmodeled, owned; RFM parameter_refinement_has_no_carrier) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../parameter_refinement_has_no_carrier.dag | 21 +++++++ src/v2/compiler/body_lowering_fold.dag | 24 +++++++- src/v2/extdeps/languages/dag.dag | 27 +++++++-- .../claim/parse/parameter_refinement_test.dag | 57 +++++++++++++++++++ .../workflow/compile_door_cause_ownership.dag | 6 ++ src/v2/workflow/floor_pure_producer_share.dag | 3 + 6 files changed, 133 insertions(+), 5 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/parameter_refinement_has_no_carrier.dag create mode 100644 src/v2/test/claim/parse/parameter_refinement_test.dag diff --git a/dag/gunbc/recurring_failure_mode/parameter_refinement_has_no_carrier.dag b/dag/gunbc/recurring_failure_mode/parameter_refinement_has_no_carrier.dag new file mode 100644 index 00000000000..f04866daf38 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/parameter_refinement_has_no_carrier.dag @@ -0,0 +1,21 @@ +module gunbc.recurring_failure_mode.parameter_refinement_has_no_carrier + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data parameter_refinement_has_no_carrier: RecurringFailureMode = RecurringFailureMode { + identity: "parameter_refinement_has_no_carrier" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a fn parameter's type is refined by a where clause (`lifetime_seconds: Int where range(min: 1, max: 3600)`), which v1 reads (`v1` `02_parse` `parse_param`), and v2 has no way to carry the refinement on a lowered parameter: the one where-clause reader (`v2.compiler.body_lowering_fold` `body_lower_kept_where_clause`) serves a type variant, and a parameter's type is read by `body_lower_type_expr_lowered_optional`, whose sequence fallback keeps the base type and drops the clause.", + "HARM: a parameter lowered without its refinement admits every value of the base type at the call boundary the author narrowed, silently -- the refinement is the parameter's contract.", + "CONTAINED, NOT SILENT: the grammar parses the refinement (`v2.extdeps.languages.dag` `dag_grammar_typed_param_expr`, the refined arm taken only where a clause is written) and body lowering refuses the fn on both arms, located at the clause, as `body_lowering_reason_parameter_refinement_unmodeled` (`body_lower_param_refinement_refusal_optional`). The module refuses at normalize.", + "RUNG FOUND AT: mitigated (typed, located refusal). CEILING: structurally impossible -- a parameter's refinement is part of its lowered type. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: a parameter's lowered type carries its where-clause refinement, read through the one where-clause reader type variants use rather than a second one, so `body_lowering_reason_parameter_refinement_unmodeled` has no producer.", + ], + + evidence: [ + DeclarationRef { module_path: "v2.test.claim.parse.parameter_refinement", decl_name: "a_refined_parameter_parses_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.parse.parameter_refinement", decl_name: "a_refined_parameter_refuses_at_its_clause_holds", field: WholeDeclaration }, + ], +} diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index cff2d6a9d0e..a5ab88a9200 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -3563,7 +3563,29 @@ fn body_lower_pattern_generics_optional(captured: Node) -> Optional { fn body_lower_first_signature_refusal_optional(captured: Node) -> Optional> { match body_lower_pattern_form_refusal_optional(captured: captured) { Present { value: refused } => optional_present(value: refused) - Absent => body_lower_fn_uses_refusal_optional(captured: captured) + Absent => + match body_lower_param_refinement_refusal_optional(captured: captured) { + Present { value: refused } => optional_present(value: refused) + Absent => body_lower_fn_uses_refusal_optional(captured: captured) + } + } +} + +// A PARAMETER WHOSE TYPE IS REFINED BY A WHERE CLAUSE REFUSES, LOCATED AT THE CLAUSE. The only +// reader of a where clause (body_lower_kept_where_clause) serves a type variant; a parameter's type +// is read by body_lower_type_expr_lowered_optional, which would keep the base type and drop the +// refinement. So until a parameter's type can carry its refinement the fn refuses +// (gunbc.recurring_failure_mode parameter_refinement_has_no_carrier). The clause is searched only +// inside this declaration's own param_list. +fn body_lower_param_refinement_refusal_optional(captured: Node) -> Optional> { + match body_lower_find_captured(root: captured, emitted: ^dag_surface_param_list) { + ParseSubtreeAbsent => optional_absent() + ParseSubtreeFound { captured: param_list } => + match body_lower_find_production_shell_optional(root: param_list, emitted: ^dag_surface_where_refinement_clause) { + Absent => optional_absent() + Present { value: clause } => + optional_present(value: outcome_rejected(d: body_lower_diagnostic(reason: ^body_lowering_reason_parameter_refinement_unmodeled, n: clause))) + } } } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index b8b42c3463a..b8946e9d1a4 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -802,12 +802,31 @@ fn dag_grammar_generic_params_expr() -> GrammarExpr { ) } +// A PARAMETER MAY REFINE ITS TYPE WITH A WHERE CLAUSE (`lifetime_seconds: Int where range(min: 1, +// max: 3600)`), as v1 02_parse parse_param reads it. The refined form is the FIRST arm and requires +// the clause, so it is taken only where one is written; an unrefined parameter falls to the second +// arm, whose shape is exactly the one every parameter reader already reads. A refined parameter +// does not lower yet: v2.compiler.body_lowering_fold refuses the fn at the clause +// (body_lowering_reason_parameter_refinement_unmodeled) rather than reading the type and dropping +// the refinement. fn dag_grammar_typed_param_expr() -> GrammarExpr { - dag_grammar_sequence( - left: dag_grammar_binding_name_terminal(), + dag_grammar_choice( + left: dag_grammar_sequence( + left: dag_grammar_binding_name_terminal(), + right: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_colon), + right: dag_grammar_sequence( + left: dag_grammar_nonterminal(production: ^dag_production_type_expr), + right: dag_grammar_nonterminal(production: ^dag_production_where_refinement_clause) + ) + ) + ), right: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_colon), - right: dag_grammar_nonterminal(production: ^dag_production_type_expr) + left: dag_grammar_binding_name_terminal(), + right: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_colon), + right: dag_grammar_nonterminal(production: ^dag_production_type_expr) + ) ) ) } diff --git a/src/v2/test/claim/parse/parameter_refinement_test.dag b/src/v2/test/claim/parse/parameter_refinement_test.dag new file mode 100644 index 00000000000..ceb35ff4f87 --- /dev/null +++ b/src/v2/test/claim/parse/parameter_refinement_test.dag @@ -0,0 +1,57 @@ +module v2.test.claim.parse.parameter_refinement + +import v2.compiler.reference_conservation_admission { conservation_subject_of_text } +import v2.extdeps.languages.dag { parse_production_emitted_identity_optional } +import v2.std.diagnostic { Accepted, NodeLocus, Rejected, diagnostics_fatal } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.optional { Absent, Present } +import v2.std.text { String } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A PARAMETER MAY REFINE ITS TYPE WITH A WHERE CLAUSE (v2.extdeps.languages.dag +// dag_grammar_typed_param_expr), as v1 reads it. It PARSES; the fn REFUSES at the clause +// (body_lowering_reason_parameter_refinement_unmodeled, gunbc.recurring_failure_mode +// parameter_refinement_has_no_carrier) rather than lowering the base type and dropping the +// refinement. An unrefined parameter is untouched. +data refined_source: String = "module probe.param_refine\n\nfn wait(seconds: Int where range(min: 1, max: 3600)) -> Int {\n seconds\n}\n" +data plain_source: String = "module probe.param_refine\n\nfn wait(seconds: Int) -> Int {\n seconds\n}\n" + +// Each outcome is computed ONCE as a nullary value, enrolled WARM in +// v2.workflow.floor_pure_producer_share, and each claim reads it. +fn refined_parsed() -> Bool { + match conservation_subject_of_text(path: "probe_refined.dag", text: refined_source).parsed { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn refined_refused_at_clause() -> Bool { + match conservation_subject_of_text(path: "probe_refined.dag", text: refined_source).normalized { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => + diagnostics_fatal(d: d).reason == ^body_lowering_reason_parameter_refinement_unmodeled + && match diagnostics_fatal(d: d).at { + NodeLocus { anchor: a } => + match parse_production_emitted_identity_optional(node: a.at) { + Present { value: id } => id == ^dag_surface_where_refinement_clause + Absent => false + } + _ => false + } + } +} + +fn plain_normalized() -> Bool { + match conservation_subject_of_text(path: "probe_plain.dag", text: plain_source).normalized { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +test fn a_refined_parameter_parses_holds() -> Bool { refined_parsed() } + +test fn a_refined_parameter_refuses_at_its_clause_holds() -> Bool { refined_refused_at_clause() } + +test fn an_unrefined_parameter_still_normalizes_holds() -> Bool { plain_normalized() } diff --git a/src/v2/workflow/compile_door_cause_ownership.dag b/src/v2/workflow/compile_door_cause_ownership.dag index 2678135a049..2f1d70fc158 100644 --- a/src/v2/workflow/compile_door_cause_ownership.dag +++ b/src/v2/workflow/compile_door_cause_ownership.dag @@ -156,6 +156,12 @@ data known_frontier_causes: List = [ lane: SharedSelfHostCriticalPath, flip_trigger: "a `pattern` declaration shares the one fn_decl production but v1 admits it only without generic params and with a block body (dag syntax dag_item_forms: has_type_params false, body_kind BlockBody); a pattern-headed declaration writing generic params or an `= expr` body refuses located at what it wrote (v2.compiler.body_lowering_fold body_lower_pattern_form_refusal_optional). This is a fidelity wall, not a frontier: it retires only if the grammar can express the narrower pattern form without changing the fn_decl spine depth the positional readers walk, so the form becomes unwritable rather than refused" }, + CauseOwnership { + cause: ^body_lowering_reason_parameter_refinement_unmodeled, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a fn parameter whose type is refined by a where clause parses and refuses at the clause on both lowering arms (v2.compiler.body_lowering_fold body_lower_param_refinement_refusal_optional), because the only where-clause reader serves a type variant and a parameter's type reader would drop the refinement. Flips when a parameter's lowered type carries its refinement -- the parameter type read through the one where-clause reader that type variants use -- so the reason has no producer (gunbc.recurring_failure_mode parameter_refinement_has_no_carrier)" + }, CauseOwnership { cause: ^body_lowering_reason_uses_clause_unmodeled, grain: FatalGrain, diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index c5b839fad7e..24c6b15320b 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -1104,6 +1104,9 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.parse.data_keyword_as_value.data_value_parsed", "v2.test.claim.parse.data_keyword_as_value.data_value_normalized", "v2.test.claim.parse.data_keyword_as_value.else_value_parsed", + "v2.test.claim.parse.parameter_refinement.refined_parsed", + "v2.test.claim.parse.parameter_refinement.refined_refused_at_clause", + "v2.test.claim.parse.parameter_refinement.plain_normalized", "v2.test.claim.occurrence_role.occurrence_role.binders_fixture_outcome", "v2.test.claim.occurrence_role.occurrence_role.mixed_param_list_parsed", "v2.test.claim.occurrence_role.occurrence_role.mixed_param_list_planted",