Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions dag/gunbc/recurring_failure_mode/uses_clause_has_no_carrier.dag
Original file line number Diff line number Diff line change
@@ -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 },
],
}
47 changes: 35 additions & 12 deletions src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -3315,13 +3317,30 @@ fn body_lower_fn_decl_exit_refusal_optional(captured: Node) -> Optional<Outcome<
}
}

// A FN THAT DECLARES A `uses` CLAUSE REFUSES, LOCATED AT THE CLAUSE, ON EVERY ROUTE. The clause is
// the fn's resource (effect) requirement and v2 has no carrier for it yet
// (gunbc.recurring_failure_mode uses_clause_has_no_carrier), so lowering the fn would drop the
// requirement. Both arms -- the full arrow and the census arrow -- ask this first, because the
// requirement is part of the signature both of them read.
fn body_lower_fn_uses_refusal_optional(captured: Node) -> Optional<Outcome<Node>> {
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<BodyLowering> {
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)
}
}
}
}
Expand Down Expand Up @@ -3571,16 +3590,20 @@ fn body_lower_fn_decl_to_census_arrow(shell: Node) -> Outcome<BodyLowering> {
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))
)
}
}
}
}
Expand Down
6 changes: 5 additions & 1 deletion src/v2/compiler/occurrence_role.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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<NameProductionRow> {
[
name_row(production: ^dag_production_fn_decl, disposition: NameRoleRead { role: DeclarationRole, category: CallableOccurrence, reader: ReadKwThenIdent }),
Expand All @@ -234,7 +237,8 @@ fn dag_name_production_rows() -> List<NameProductionRow> {
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 })
]
}

Expand Down
83 changes: 72 additions & 11 deletions src/v2/extdeps/languages/dag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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
Expand All @@ -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
)
)
)
)
Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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,
Expand Down
60 changes: 60 additions & 0 deletions src/v2/test/claim/parse/uses_clause_test.dag
Original file line number Diff line number Diff line change
@@ -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 }
6 changes: 6 additions & 0 deletions src/v2/workflow/compile_door_cause_ownership.dag
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,12 @@ data known_frontier_causes: List<CauseOwnership> = [
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,
Expand Down
2 changes: 2 additions & 0 deletions src/v2/workflow/floor_pure_producer_share.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1076,6 +1076,8 @@ data floor_cross_claim_pure_producers_warm: List<String> = [
"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",
Expand Down