diff --git a/dag/gunbc/recurring_failure_mode/uses_clause_has_no_carrier.dag b/dag/gunbc/recurring_failure_mode/uses_clause_has_no_carrier.dag new file mode 100644 index 00000000000..6232448425d --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/uses_clause_has_no_carrier.dag @@ -0,0 +1,21 @@ +module gunbc.recurring_failure_mode.uses_clause_has_no_carrier + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data uses_clause_has_no_carrier: RecurringFailureMode = RecurringFailureMode { + identity: "uses_clause_has_no_carrier" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a fn declaration's `uses` clause (`uses net: Network, fs: Filesystem`) states the resources the fn requires, and v2 has no carrier for that requirement: no field of the lowered Arrow, no effect-requirement type the declaration lowers onto. v1 reads it (`v1` `02_parse` `parse_uses_clause`, a resource-use node per entry) and v1's CLI admits a resource method only where the fn declares that resource there, so it is a semantic fact, not trivia.", + "HARM: a lowering that parsed the clause and dropped it would erase an effect requirement silently -- a fn would lower as if it used no resource, and nothing downstream could refuse a resource method it calls. Until this lands, such fns cannot be observed by the v2 route at all.", + "CONTAINED, NOT SILENT: the grammar parses the clause (`v2.extdeps.languages.dag` `dag_grammar_uses_clause_expr`) and body lowering refuses every fn carrying one on BOTH arms, full and census, located at the clause, as `body_lowering_reason_uses_clause_unmodeled` (`v2.compiler.body_lowering_fold` `body_lower_fn_uses_refusal_optional`). The module refuses at normalize; it never lowers without its requirement. These modules are therefore outside the XL-2 reference census until the carrier exists.", + "RUNG FOUND AT: mitigated (typed, located refusal; the module refuses at normalize). CEILING: structurally impossible -- a fn's resource requirement is a field of its lowered signature, so a lowered fn cannot exist without it. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: a v2 effect-requirement carrier on the lowered fn signature that body lowering reads each `uses` entry onto (name, resource type, config), so that every fn in the corpus that declares a `uses` clause lowers with its requirement and `body_lowering_reason_uses_clause_unmodeled` has no producer.", + ], + + evidence: [ + DeclarationRef { module_path: "v2.test.claim.parse.uses_clause", decl_name: "a_fn_with_a_uses_clause_parses_holds", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.claim.parse.uses_clause", decl_name: "a_fn_with_a_uses_clause_refuses_at_the_clause_holds", field: WholeDeclaration }, + ], +} diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index c257170f480..6802155db55 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -700,6 +700,8 @@ fn body_lower_is_structure_preserved_emitted(emitted: Symbol) -> Bool { || (emitted == ^dag_surface_field_decl_block) || (emitted == ^dag_surface_positional_variant_payload) || (emitted == ^dag_surface_admit_callers_clause) + || (emitted == ^dag_surface_uses_clause) + || (emitted == ^dag_surface_uses_entry) || (emitted == ^dag_surface_fn_type) || (emitted == ^dag_surface_field_init) || (emitted == ^dag_surface_where_refinement_clause) @@ -3315,13 +3317,30 @@ fn body_lower_fn_decl_exit_refusal_optional(captured: Node) -> Optional Optional> { + match body_lower_find_production_shell_optional(root: captured, emitted: ^dag_surface_uses_clause) { + Absent => optional_absent() + Present { value: clause } => + optional_present(value: outcome_rejected(d: body_lower_diagnostic(reason: ^body_lowering_reason_uses_clause_unmodeled, n: clause))) + } +} + fn body_lower_fn_decl_to_arrow(shell: Node) -> Outcome { match body_lower_unwrap_captured(shell: shell) { Absent => body_lower_wrapper_retained_shell(shell: shell) Present { value: captured } => - match body_lower_fn_decl_exit_refusal_optional(captured: captured) { + match body_lower_fn_uses_refusal_optional(captured: captured) { Present { value: refused } => body_lowering_lowered(o: refused) - Absent => body_lower_fn_decl_to_arrow_admitted(shell: shell, captured: captured) + Absent => + match body_lower_fn_decl_exit_refusal_optional(captured: captured) { + Present { value: refused } => body_lowering_lowered(o: refused) + Absent => body_lower_fn_decl_to_arrow_admitted(shell: shell, captured: captured) + } } } } @@ -3571,16 +3590,20 @@ fn body_lower_fn_decl_to_census_arrow(shell: Node) -> Outcome { match body_lower_unwrap_captured(shell: shell) { Absent => body_lower_wrapper_retained_shell(shell: shell) Present { value: captured } => - match body_lower_fn_signature_optional(captured: captured) { - Rejected { diagnostics: r } => body_lowering_lowered(o: Rejected { diagnostics: r }) - Accepted { value: Absent, diagnostics: _ } => body_lower_wrapper_retained_shell(shell: shell) - Accepted { value: Present { value: sig }, diagnostics: _ } => - match body_lower_fn_signature_refusal(shell: shell, sig: sig) { - Present { value: refused } => body_lowering_lowered(o: refused) - Absent => - body_lowering_lowered( - o: outcome_accepted(value: body_lower_fn_decl_arrow(shell: shell, sig: sig, body: Absent)) - ) + match body_lower_fn_uses_refusal_optional(captured: captured) { + Present { value: refused } => body_lowering_lowered(o: refused) + Absent => + match body_lower_fn_signature_optional(captured: captured) { + Rejected { diagnostics: r } => body_lowering_lowered(o: Rejected { diagnostics: r }) + Accepted { value: Absent, diagnostics: _ } => body_lower_wrapper_retained_shell(shell: shell) + Accepted { value: Present { value: sig }, diagnostics: _ } => + match body_lower_fn_signature_refusal(shell: shell, sig: sig) { + Present { value: refused } => body_lowering_lowered(o: refused) + Absent => + body_lowering_lowered( + o: outcome_accepted(value: body_lower_fn_decl_arrow(shell: shell, sig: sig, body: Absent)) + ) + } } } } diff --git a/src/v2/compiler/occurrence_role.dag b/src/v2/compiler/occurrence_role.dag index a9fb0c8ff79..9d8ac4d1268 100644 --- a/src/v2/compiler/occurrence_role.dag +++ b/src/v2/compiler/occurrence_role.dag @@ -210,6 +210,9 @@ fn read_names(reader: NameReader, captured: Node) -> NameRead { // `operation name { .. }`: body lowering reads the name with the kw-then-ident decoder // (body_lower_operation), and lowers it to a callable edge of the service. +// `uses net: Network`: each entry binds the resource name the fn body refers to. Its shape is +// `name: T [(cfg)]`, the `name: value` pair ReadFieldInitLabel's decoder reads, so it is read by that +// decoder, and the binder is a declaration. fn dag_name_production_rows() -> List { [ name_row(production: ^dag_production_fn_decl, disposition: NameRoleRead { role: DeclarationRole, category: CallableOccurrence, reader: ReadKwThenIdent }), @@ -234,7 +237,8 @@ fn dag_name_production_rows() -> List { name_row(production: ^dag_production_arrow_lambda, disposition: NameRoleRead { role: DeclarationRole, category: LexicalValueOccurrence, reader: ReadFunctionValueBinders { kind: ArrowLambdaValue } }), name_row(production: ^dag_production_operation, disposition: NameRoleRead { role: DeclarationRole, category: CallableOccurrence, reader: ReadKwThenIdent }), name_row(production: ^dag_production_input_block, disposition: NameRoleRead { role: DeclarationRole, category: FieldOccurrence, reader: ReadIoFieldBinders }), - name_row(production: ^dag_production_output_block, disposition: NameRoleRead { role: DeclarationRole, category: FieldOccurrence, reader: ReadIoFieldBinders }) + name_row(production: ^dag_production_output_block, disposition: NameRoleRead { role: DeclarationRole, category: FieldOccurrence, reader: ReadIoFieldBinders }), + name_row(production: ^dag_production_uses_entry, disposition: NameRoleRead { role: DeclarationRole, category: LexicalValueOccurrence, reader: ReadFieldInitLabel }) ] } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 2d2c4ee0952..631601ecb74 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -1948,6 +1948,49 @@ fn dag_grammar_data_decl_expr() -> GrammarExpr { // else. The clause is consumed and then DISCARDED when the fn lowers to an Arrow: nothing on the // native route checks caller admission, and the stage that does adds its Arrow carrier together // with that consumer (gunbc.rung_drop admit_callers_discarded_on_the_native_route). +// `uses net: Network, fs: Filesystem` after a fn's return clause declares the resources the fn +// requires, as v1 02_parse parse_uses_clause reads it: one or more comma-separated entries, each a +// name, a type and an optional parenthesised config. `uses` is matched as an exact-word terminal and +// stays an ordinary identifier everywhere else. The clause PARSES; it does not lower yet: v2 has no +// carrier for a fn's resource requirement, so v2.compiler.body_lowering_fold refuses every fn that +// carries one, located at the clause (body_lowering_reason_uses_clause_unmodeled), rather than +// lowering the fn and dropping the requirement. +fn dag_grammar_uses_clause_expr() -> GrammarExpr { + dag_grammar_sequence( + left: dag_grammar_literal_terminal(token_class: ^dag_token_ident, lexeme: symbol_intern_lexeme(lexeme: "uses")), + right: dag_grammar_sequence( + left: dag_grammar_nonterminal(production: ^dag_production_uses_entry), + right: dag_grammar_repeat( + element: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_comma), + right: dag_grammar_nonterminal(production: ^dag_production_uses_entry) + ) + ) + ) + ) +} + +fn dag_grammar_uses_entry_expr() -> GrammarExpr { + 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_optional( + element: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_lparen), + right: dag_grammar_sequence( + left: dag_grammar_field_init_list_helper(), + right: dag_grammar_terminal(token_class: ^dag_token_rparen) + ) + ) + ) + ) + ) + ) +} + fn dag_grammar_admit_callers_clause_expr() -> GrammarExpr { dag_grammar_sequence( left: dag_grammar_literal_terminal( @@ -1987,9 +2030,10 @@ fn dag_grammar_admit_callers_clause_expr() -> GrammarExpr { // is gunbc.recurring_failure_mode a_positional_fact_is_obtained_by_searching_for_its_shape. // // WHAT THAT READER RELIES ON, stated so it is checkable rather than folded into its own comment: -// this production has THREE optionals, and only generic_params precedes the return clause, so -// generic_params is the entire risk surface for the depth. The admit_callers clause is the third -// and sits AFTER the return clause, so it does not shift the depth this reader walks. +// this production has FOUR optionals, and only generic_params precedes the return clause, so +// generic_params is the entire risk surface for the depth. The uses clause and the admit_callers +// clause are the third and fourth and sit AFTER the return clause, so they do not shift the depth +// this reader walks. // An elided optional still occupies // its slot -- v2.compiler.parse `parse_expr_optional` returns grammar_empty_node on the rejected // arm -- so the depth does not shift when it is absent. Both arms are held by executing claims in @@ -2015,15 +2059,20 @@ fn dag_grammar_fn_decl_expr() -> GrammarExpr { ), right: dag_grammar_sequence( left: dag_grammar_optional( - element: dag_grammar_nonterminal(production: ^dag_production_admit_callers_clause) + element: dag_grammar_nonterminal(production: ^dag_production_uses_clause) ), - right: dag_grammar_choice( - left: dag_grammar_nonterminal(production: ^dag_production_fn_body), - right: dag_grammar_sequence( - left: dag_grammar_terminal(token_class: ^dag_token_eq), - right: dag_grammar_expect( - element: dag_grammar_nonterminal(production: ^dag_production_expr), - reason: FnExpressionBodyMissingAfterEq + right: dag_grammar_sequence( + left: dag_grammar_optional( + element: dag_grammar_nonterminal(production: ^dag_production_admit_callers_clause) + ), + right: dag_grammar_choice( + left: dag_grammar_nonterminal(production: ^dag_production_fn_body), + right: dag_grammar_sequence( + left: dag_grammar_terminal(token_class: ^dag_token_eq), + right: dag_grammar_expect( + element: dag_grammar_nonterminal(production: ^dag_production_expr), + reason: FnExpressionBodyMissingAfterEq + ) ) ) ) @@ -2754,6 +2803,16 @@ fn dag_grammar_root() -> GrammarRoot { expression: dag_grammar_else_less_if_stmt_expr(), emitted: ^dag_surface_else_less_if_stmt ) + let uses_clause = dag_grammar_production( + name: ^dag_production_uses_clause, + expression: dag_grammar_uses_clause_expr(), + emitted: ^dag_surface_uses_clause + ) + let uses_entry = dag_grammar_production( + name: ^dag_production_uses_entry, + expression: dag_grammar_uses_entry_expr(), + emitted: ^dag_surface_uses_entry + ) let admit_callers_clause = dag_grammar_production( name: ^dag_production_admit_callers_clause, expression: dag_grammar_admit_callers_clause_expr(), @@ -2910,6 +2969,8 @@ fn dag_grammar_root() -> GrammarRoot { import_block, field_decl_block, positional_variant_payload, + uses_clause, + uses_entry, admit_callers_clause, else_less_if_stmt, fn_body, diff --git a/src/v2/test/claim/parse/uses_clause_test.dag b/src/v2/test/claim/parse/uses_clause_test.dag new file mode 100644 index 00000000000..19074744051 --- /dev/null +++ b/src/v2/test/claim/parse/uses_clause_test.dag @@ -0,0 +1,60 @@ +module v2.test.claim.parse.uses_clause + +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 FN MAY DECLARE v1's `uses` CLAUSE (v2.extdeps.languages.dag dag_grammar_uses_clause_expr). It +// PARSES; it does not lower: v2 has no carrier for a fn's resource requirement, so normalize refuses +// the fn located at the clause (body_lowering_reason_uses_clause_unmodeled, +// gunbc.recurring_failure_mode uses_clause_has_no_carrier) rather than lowering it without the +// requirement. +data uses_source: String = "module probe.uses\n\nfn fetch(n: Int) -> Int\n uses net: Network, fs: Filesystem\n = 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 (a claim that parsed its own source +// is over the new-witness eval-step budget). +fn uses_parsed() -> Bool { + match conservation_subject_of_text(path: "probe_uses.dag", text: uses_source).parsed { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +// The normalize refusal's reason, and whether it is anchored at the clause. A lowering refusal is a +// NodeLocus (v2.std.diagnostic node_locus), so "located at the clause" means its anchor IS the +// uses_clause production shell, not the fn around it. +type UsesRefusal { + is_unmodeled: Bool + at_clause: Bool +} + +fn uses_refusal() -> UsesRefusal { + match conservation_subject_of_text(path: "probe_uses.dag", text: uses_source).normalized { + Accepted { value: _, diagnostics: _ } => UsesRefusal { is_unmodeled: false, at_clause: false } + Rejected { diagnostics: d } => + UsesRefusal { + is_unmodeled: diagnostics_fatal(d: d).reason == ^body_lowering_reason_uses_clause_unmodeled, + at_clause: match diagnostics_fatal(d: d).at { + NodeLocus { anchor: a } => + match parse_production_emitted_identity_optional(node: a.at) { + Present { value: id } => id == ^dag_surface_uses_clause + Absent => false + } + _ => false + } + } + } +} + +test fn a_fn_with_a_uses_clause_parses_holds() -> Bool { uses_parsed() } + +test fn a_fn_with_a_uses_clause_refuses_at_the_clause_holds() -> Bool { uses_refusal().is_unmodeled } + +test fn the_uses_refusal_is_located_at_the_clause_holds() -> Bool { uses_refusal().at_clause } diff --git a/src/v2/workflow/compile_door_cause_ownership.dag b/src/v2/workflow/compile_door_cause_ownership.dag index 9584ab55c90..67645884db9 100644 --- a/src/v2/workflow/compile_door_cause_ownership.dag +++ b/src/v2/workflow/compile_door_cause_ownership.dag @@ -150,6 +150,12 @@ data known_frontier_causes: List = [ lane: SharedSelfHostCriticalPath, flip_trigger: "a service declaration lowers at declaration grade (v2.compiler.body_lowering_fold body_lower_service_decl) and its realization and unmodeled interface members are set aside; full normalize refuses a closure member carrying any, because resolution, eval and emission would have to assume them. Flips when a realization binding carrier (a transport handler bound to the interface shape) and a typed operation-modifier carrier exist, so that no set-aside reason has a producer (gunbc.recurring_failure_mode service_interface_member_has_no_carrier)" }, + CauseOwnership { + cause: ^body_lowering_reason_uses_clause_unmodeled, + grain: FatalGrain, + lane: SharedSelfHostCriticalPath, + flip_trigger: "a fn declaring a `uses` clause parses and refuses at the clause on both lowering arms (v2.compiler.body_lowering_fold body_lower_fn_uses_refusal_optional), because v2 has no carrier for a fn's resource requirement and lowering the fn would drop it. Flips when a lowered fn signature carries every `uses` entry's resource requirement -- a v2 effect-requirement carrier that body lowering reads each entry onto (name, resource type, config) -- so the reason has no producer (gunbc.recurring_failure_mode uses_clause_has_no_carrier)" + }, CauseOwnership { cause: ^body_lowering_reason_field_decl_unlowered, grain: FatalGrain, diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index bdd174c4c24..9375fe28c0f 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -1076,6 +1076,8 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.parse.block_expr_as_binary_operand_parse.ordinary_binary_parsed", "v2.test.parse.block_expr_as_binary_operand_parse.bare_match_body_is_match", "v2.test.parse.block_expr_as_binary_operand_parse.bare_if_body_is_branch", + "v2.test.claim.parse.uses_clause.uses_parsed", + "v2.test.claim.parse.uses_clause.uses_refusal", "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",