diff --git a/dag/gunbc/guarantee_stall/member_kind_door_binding_executed_by_no_claim_stall.dag b/dag/gunbc/guarantee_stall/member_kind_door_binding_executed_by_no_claim_stall.dag new file mode 100644 index 00000000000..15a0f4cb8f4 --- /dev/null +++ b/dag/gunbc/guarantee_stall/member_kind_door_binding_executed_by_no_claim_stall.dag @@ -0,0 +1,25 @@ +module gunbc.guarantee_stall.member_kind_door_binding_executed_by_no_claim_stall + +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when } + +// A NEW LINK THAT HAS NEVER EXECUTED, RECORDED AS A STALL -- NOT A DROP: no rung stood here and none is claimed to have +// fallen. gunbc#13513 carries the authored data-vs-fn kind from normalize to the mandatory_tag gate +// (NormalizedTree.member_declarations -> member_kind_channel_of_tree -> ResolvedTree.member_kinds). The legs +// normalize -> member_kind_channel_of_tree -> gate execute in test.long.mandatory_tag_gate_witness. The leg from +// v2.compiler.name_resolve resolve_in_context (subject_member_kind_channel) through ResolvedTree.member_kinds to +// v2.compiler.compile validate_then_compile's mandatory_tag_root_lens_with_provenance binding is compiled and +// typechecked and executed by no claim: a door-grain control through compile_source_root_ingest_with_admission was +// refused with member_not_a_binder by a roster lens ahead of mandatory_tag on even a trivial single-module extdeps.* +// subject, a refusal independent of #13513 and filed as its own item. Each removed door-grain witness measured roughly +// 470-560k eval steps against the 72300 new-witness budget, so it is a long-lane witness once runnable. +data member_kind_door_binding_executed_by_no_claim_stall: GuaranteeStall = GuaranteeStall { + subject: "door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> validate_then_compile mandatory_tag_root_lens_with_provenance link is executed by no claim", + current: Mitigatable, + ceiling: MechanicallyPreventable, + blocker: AwaitsOneGrounding { grounding: "the door accepting a minimal extdeps.* subject past every roster lens (the member_not_a_binder door refusal, its own item), which makes the door-grain controls runnable" }, + population: BoundedPopulation { members: [ + "v2.compiler.name_resolve resolve_in_context subject_member_kind_channel -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission" + ] }, + next_rung_trigger: climbs_when(capability: "a minimal extdeps.* subject is accepted through compile_source_root_ingest_with_admission past every roster lens, and the door-grain mandatory_tag clean and zero-arg-fn impersonation controls execute on the long lane. SUFFICIENT FOR: deleting the ResolvedTree.member_kinds binding (or resolve_in_context's subject_member_kind_channel) turns a door-grain control red. A control that supplies the channel, runs a lens directly, or reaches the gate below the door retires nothing") +} diff --git a/dag/gunbc/guarantee_stall/roster.dag b/dag/gunbc/guarantee_stall/roster.dag index 2240a5c4741..10bf7855a40 100644 --- a/dag/gunbc/guarantee_stall/roster.dag +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -76,6 +76,7 @@ import gunbc.guarantee_stall.text_carrier_render_not_keyed_on_identity_stall { t import gunbc.guarantee_stall.free_semigroup_text_crossing_decided_by_spelling_stall { free_semigroup_text_crossing_decided_by_spelling_stall } import gunbc.guarantee_stall.emitted_inline_crate_path_edges_unreturned_stall { emitted_inline_crate_path_edges_unreturned_stall } import gunbc.guarantee_stall.compile_pool_provision_wired_but_unreachable_stall { compile_pool_provision_wired_but_unreachable_stall } +import gunbc.guarantee_stall.member_kind_door_binding_executed_by_no_claim_stall { member_kind_door_binding_executed_by_no_claim_stall } import gunbc.guarantee_stall.filesystem_read_outcome_node_grain_census_stall { filesystem_read_outcome_node_grain_census_stall } // THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are @@ -248,6 +249,7 @@ data all_guarantee_stalls: List = [ browser_ready_labels_fleet_route_stall, accumulator_copy_untyped_combiner_refusals_stall, keyed_apply_patch_rebuilds_rows_per_hunk_stall, + member_kind_door_binding_executed_by_no_claim_stall, filesystem_read_outcome_node_grain_census_stall, ] diff --git a/src/v2/compiler/00_compile.dag b/src/v2/compiler/00_compile.dag index c39846fb6cd..b84fb9f7a5e 100644 --- a/src/v2/compiler/00_compile.dag +++ b/src/v2/compiler/00_compile.dag @@ -200,7 +200,8 @@ import v2.extdeps.languages.dag { import v2.lens.complexity_accumulator_copy.compile_gate { accumulator_copy_compile_gate } import v2.lens.determinism { determinism_compile_gate } import v2.lens.machine_shape { machine_shape_compile_gate } -import v2.lens.mandatory_tag { mandatory_tag_compile_gate } +import v2.lens.mandatory_tag { mandatory_tag_compile_gate, mandatory_tag_compile_gate_with_provenance } +import v2.std.member_declaration_kind { MemberKindChannel, no_member_declaration_kinds } import v2.lens.undecidable_verdict_collapse { undecidable_verdict_collapse_compile_gate } import v2.lens.fact_density { fact_density_hollow_alias_gate } import v2.lens.unit_modeling { unit_modeling_gate } @@ -795,6 +796,20 @@ fn machine_shape_root_gate(tree: InferredTree) -> Outcome> { machine_shape_compile_gate(node: tree.root) } +// The compile door's binding of the mandatory_tag gate: the same gate, handed the member-kind provenance +// the resolved subject carries (ResolvedTree.member_kinds). +fn mandatory_tag_root_lens_with_provenance(lens: CompileLens, channel: MemberKindChannel) -> CompileLens { + if lens.identity == mandatory_tag_lens.identity { + CompileLens { + identity: lens.identity, + grain: lens.grain, + gate: fn(tree) { mandatory_tag_compile_gate_with_provenance(node: tree.root, channel: channel) } + } + } else { + lens + } +} + fn mandatory_tag_root_gate(tree: InferredTree) -> Outcome> { mandatory_tag_compile_gate(node: tree.root) } @@ -1042,9 +1057,13 @@ fn validate_then_compile( bind_outcome( o: run_required_lens_gates( inferred: inferred, - lenses: list_append( - left: required_lenses_at_grain(grain: CompileLensRoot), - right: lenses_at_grain(lenses: lenses, grain: CompileLensRoot) + lenses: fold( + list_append( + left: required_lenses_at_grain(grain: CompileLensRoot), + right: lenses_at_grain(lenses: lenses, grain: CompileLensRoot) + ), + init: [], + f: fn(acc, l) { list_snoc_item(xs: acc, item: mandatory_tag_root_lens_with_provenance(lens: l, channel: source.member_kinds)) } ) ), f: fn(root_witnesses) { @@ -3506,6 +3525,7 @@ fn native_module_resolve_verdict( symbol_index: shared.symbol_index, closure_declarations: closure.declarations, unavailable_providers: closure.refused, + member_kinds: no_member_declaration_kinds(), lexical: lexical ) }, diff --git a/src/v2/compiler/03_ingest.dag b/src/v2/compiler/03_ingest.dag index 070cf7ea6e3..ea2e978d147 100644 --- a/src/v2/compiler/03_ingest.dag +++ b/src/v2/compiler/03_ingest.dag @@ -38,6 +38,7 @@ import v2.compiler.translate { coerce_grounded_node } import v2.compiler.target_serialize { target_bundle_child } import v2.std.inhabitant_neutralization { neutralize_core_for_target } import v2.std.node { Edge, Authored, StructuralLabel, Node, Positional, Symbol, TypeNode, Conj } +import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.std.diagnostic { Accepted, Diagnostic, @@ -337,7 +338,7 @@ fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: Target o: parse_tree_to_emitted_node(parse_tree: parse_tree, source_model: source_model), f: fn(emitted) { bind_outcome( - o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] }), + o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() }), f: fn(inferred) { bind_outcome( o: coerce_grounded_node(source: emitted, tree: inferred, target: source_model), @@ -362,7 +363,7 @@ fn cross_language_compile( o: neutralize_core_for_target(core: core, target: target_model), f: fn(neutralized) { bind_outcome( - o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] }), + o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() }), f: fn(inferred) { emit(tree: inferred, target: target_model) } diff --git a/src/v2/compiler/03_name_resolve.dag b/src/v2/compiler/03_name_resolve.dag index 04c93a6c8ca..931c44fae5e 100644 --- a/src/v2/compiler/03_name_resolve.dag +++ b/src/v2/compiler/03_name_resolve.dag @@ -2,6 +2,7 @@ module v2.compiler.name_resolve import std.types { List } import v2.std.language_model { LanguageModel } +import v2.std.member_declaration_kind { MemberKindChannel, no_member_declaration_kinds } import v2.compiler.symbol_index_fill { symbol_index_fill_module_declarations, symbol_index_fill_module_roots } import v2.compiler.normalized_tree { NormalizedTree, normalized_tree_roots_to_binding_sources } @@ -16,6 +17,7 @@ import v2.compiler.resolve { ResolveNodeWalk, ResolveWalkRefused, ClosureProviderRefusal, + member_kind_channel_of_tree, ResolvedTree, resolved_tree_outcome, resolve_walk_prefix_pending, @@ -695,6 +697,16 @@ fn subject_module_root_for_name( } } +// The subject root's member-kind channel, read from the validated roots by the subject's own name. A subject +// with no root there has no provenance to give, which is Unavailable and not a refusal here: the module-not-found +// refusal already belongs to admission. +fn subject_member_kind_channel(roots: ValidatedModuleRoots, name: QualifiedName) -> Outcome { + match map_lookup(m: roots.by_name, key: name) { + Present { value: root } => member_kind_channel_of_tree(tree: root) + Absent => Accepted { value: no_member_declaration_kinds(), diagnostics: v2.std.diagnostic.None } + } +} + fn namespace_admission_initial_state( policy: NameResolutionPolicy, canonical_symbols: PointwisePower, @@ -936,12 +948,17 @@ fn resolve_in_context(context: Outcome, admission: Admission) Accepted { value: shared, diagnostics: d } => let closure = closure_declarations_demand(shared: shared) ContextResolved { - resolved: resolved_tree_outcome( - w: walked.walk, - symbol_index: shared.symbol_index, - closure_declarations: closure.declarations, - unavailable_providers: closure.refused - ), + resolved: match subject_member_kind_channel(roots: shared.roots, name: admission.subject.name) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: channel, diagnostics: _ } => + resolved_tree_outcome( + w: walked.walk, + symbol_index: shared.symbol_index, + closure_declarations: closure.declarations, + unavailable_providers: closure.refused, + member_kinds: channel + ) + }, context: Accepted { value: closure.context, diagnostics: d } } } diff --git a/src/v2/compiler/03_normalize.dag b/src/v2/compiler/03_normalize.dag index 6f596597c4d..d10704db656 100644 --- a/src/v2/compiler/03_normalize.dag +++ b/src/v2/compiler/03_normalize.dag @@ -75,15 +75,23 @@ import v2.compiler.normalized_tree { NormalizedTree, admit_census_tree, admit_normalized_tree, - admit_retention_free + admit_retention_free, + normalized_tree_with_member_declarations } +import v2.std.member_declaration_kind { DeclaredDataMember, DeclaredFnMember, DeclaredMember } import v2.compiler.test_marker_capture { test_marker_capture } import v2.compiler.namespace_graft { module_header_containment_graft, - namespace_graft_is_graft_candidate + namespace_graft_collect_unit_nodes_against, + namespace_graft_is_graft_candidate, + namespace_graft_top_level_item_alternative_emitted_ids } import v2.extdeps.languages.dag { + dag_grammar_root, + dag_surface_kw_then_ident_from_captured, import_binding_rows_from_decl_node, + namespace_graft_unwrap_module_working_root, + parse_production_captured_child_optional, parse_production_emitted_identity_optional } import std.types { List } @@ -408,6 +416,47 @@ fn type_declaration_kind_capture(nodes: List) -> FreeMonoid T { v }` into one shape (a named nullary Arrow), so +// after normalize nothing in the Node says which was authored. The population is the graft's own unit +// census (namespace_graft_collect_unit_nodes_against over the module's working root, the same units the +// graft partitions into members), NOT every node of the parse: a declaration nested in another unit is +// not a member of the module. A data or fn unit whose name cannot be read contributes no row, so a +// consumer asking for it finds it not declared and refuses, never a fabricated kind. +// v2.std.member_declaration_kind MemberKindChannel is what carries these to a later grain. +fn member_declaration_capture(tree: ParseTree) -> FreeMonoid { + let unit_ids = namespace_graft_top_level_item_alternative_emitted_ids(productions: dag_grammar_root().productions) + fold_list( + xs: namespace_graft_collect_unit_nodes_against(node: namespace_graft_unwrap_module_working_root(root: tree), unit_ids: unit_ids), + empty: Empty, + cons: fn(acc, unit) { + match parse_production_emitted_identity_optional(node: unit) { + Absent => acc + Present { value: id } => + if (id == ^dag_surface_data_decl) || (id == ^dag_surface_fn_decl) { + match parse_production_captured_child_optional(node: unit) { + Absent => acc + Present { value: captured } => + match dag_surface_kw_then_ident_from_captured(captured: captured) { + Absent => acc + Present { value: name } => + list_snoc_item( + xs: acc, + item: DeclaredMember { + name: name, + kind: if id == ^dag_surface_data_decl { DeclaredDataMember } else { DeclaredFnMember } + } + ) + } + } + } else { + acc + } + } + } + ) +} + // WHICH MODIFIERS EACH TYPE DECLARATION'S SLOT CARRIES, read from the parse tree for the reason // type_declaration_kind_capture is: lowering leaves no trace of the slot in the node. The question is // answered by the lowering's own reader (v2.compiler.body_lowering_fold @@ -507,7 +556,13 @@ fn normalize_with(parse_tree: ParseTree, source: NormalizeAllocatorSource) -> Ou ) { Rejected { diagnostics: r } => Rejected { diagnostics: r } Accepted { value: tree, diagnostics: d2 } => - Accepted { value: ScopedNormalizedTree { tree: tree, allocator: allocated.allocator }, diagnostics: d2 } + Accepted { + value: ScopedNormalizedTree { + tree: normalized_tree_with_member_declarations(tree: tree, members: member_declaration_capture(tree: parse_tree)), + allocator: allocated.allocator + }, + diagnostics: d2 + } } } } diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index cda409b2df4..b45b7ff6e16 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -1,7 +1,16 @@ module v2.compiler.resolve import v2.std.language_model { LanguageModel } -import v2.compiler.normalized_tree { NormalizedTree, normalized_tree_resource_declarations } +import v2.compiler.normalized_tree { MemberDeclarationsNotRead, MemberDeclarationsRead, NormalizedTree, normalized_tree_resource_declarations } +import v2.std.member_declaration_kind { + DeclaredMember, + declared_members_have_duplicate, + MemberKindChannel, + MemberKindsCaptured, + MemberKindsUnavailable, + QualifiedDeclaredMember, + no_member_declaration_kinds +} import v2.compiler.namespace_graft { namespace_graft_module_body_optional } import v2.std.declaration_marker { ReachesNoTestCode, @@ -258,6 +267,7 @@ type ResolvedTree { resolved_declarations: SymbolIndex lexical_bindings: Map unavailable_providers: List + member_kinds: MemberKindChannel } // A CLOSURE ROOT WHOSE OWN RESOLVE REFUSED, AND WHY. v2.compiler.name_resolve closure_declarations_demand @@ -328,6 +338,7 @@ fn resolved_tree_of( symbol_index: SymbolIndex, closure_declarations: SymbolIndex, unavailable_providers: List, + member_kinds: MemberKindChannel, lexical: List ) -> ResolvedTree { ResolvedTree { @@ -335,7 +346,49 @@ fn resolved_tree_of( symbol_index: symbol_index, resolved_declarations: resolved_declarations_over(closure: closure_declarations, subject: root), lexical_bindings: fold(lexical, init: empty_map(), f: fn(m, e) { map_insert(m, e.reference, e.binding) }), - unavailable_providers: unavailable_providers + unavailable_providers: unavailable_providers, + member_kinds: member_kinds + } +} + +// THE SUBJECT'S MEMBER-KIND CHANNEL, keyed by the DECLARING path (this module's qualified name + the member's +// name). The channel covers the subject module only -- the one root mandatory_tag runs on -- so resolve pays +// one pass over one module's members, not one per root in the closure. A tree normalize read no members for +// (a hand-built root) is Unavailable, never an empty captured list. Roots are unique by name already +// (ModuleRootsDuplicate refuses a second root for one module), so the only merge that can conflict is two +// members of one module sharing a name: that refuses, located at the root, and is never first-wins. +fn member_kind_channel_of_tree(tree: NormalizedTree) -> Outcome { + match tree.member_declarations { + MemberDeclarationsNotRead => Accepted { value: no_member_declaration_kinds(), diagnostics: None } + MemberDeclarationsRead { members: members } => + match qualified_name_from_module_node(root: tree.root) { + Rejected { diagnostics: _ } => Accepted { value: no_member_declaration_kinds(), diagnostics: None } + Accepted { value: module_qn, diagnostics: _ } => + let duplicated = declared_members_have_duplicate(members: members) + if duplicated { + Rejected { + diagnostics: diagnostics_singleton( + d: Diagnostic { + reason: ^resolve_reason_member_kind_duplicate_declaration, + at: node_locus(node: tree.root), + correction: Unavailable { reason: ExternalContractUnknown } + } + ) + } + } else { + Accepted { + value: MemberKindsCaptured { + covered: [module_qn], + members: fold_list( + xs: members, + empty: [], + cons: fn(acc, m) { list_snoc_item(xs: acc, item: QualifiedDeclaredMember { module: module_qn, name: m.name, kind: m.kind }) } + ) + }, + diagnostics: None + } + } + } } } @@ -2355,12 +2408,13 @@ fn resolved_tree_outcome( w: ResolveNodeWalk, symbol_index: SymbolIndex, closure_declarations: SymbolIndex, - unavailable_providers: List + unavailable_providers: List, + member_kinds: MemberKindChannel ) -> Outcome { match w { ResolveWalkAccepted { value: v, diagnostics: d, lexical: l } => Accepted { - value: resolved_tree_of(root: v, symbol_index: symbol_index, closure_declarations: closure_declarations, unavailable_providers: unavailable_providers, lexical: l), + value: resolved_tree_of(root: v, symbol_index: symbol_index, closure_declarations: closure_declarations, unavailable_providers: unavailable_providers, member_kinds: member_kinds, lexical: l), diagnostics: d } ResolveWalkRefused { first: f, rest: _, observation: _ } => Rejected { diagnostics: f } @@ -4409,7 +4463,10 @@ fn resolve_with_namespace_policy( lm: LanguageModel, policy: NameResolutionPolicy ) -> Outcome { - resolved_tree_outcome( + match member_kind_channel_of_tree(tree: tree) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: channel, diagnostics: _ } => + resolved_tree_outcome( w: resolve_walk_with_namespace_policy( tree: tree, namespace: namespace, @@ -4418,8 +4475,10 @@ fn resolve_with_namespace_policy( ), symbol_index: namespace.symbol_index, closure_declarations: empty_symbol_index(), - unavailable_providers: [] + unavailable_providers: [], + member_kinds: channel ) + } } fn resolve_walk_with_namespace_policy( diff --git a/src/v2/compiler/normalized_tree.dag b/src/v2/compiler/normalized_tree.dag index 0cea14bba87..c4c6714c7aa 100644 --- a/src/v2/compiler/normalized_tree.dag +++ b/src/v2/compiler/normalized_tree.dag @@ -26,6 +26,7 @@ import std.algebra { Cons, Empty, FreeMonoid, list_snoc_item } import v2.std.algebra { fold_list } import v2.std.node { Edge, Node, Symbol, content_hash } import v2.std.declaration_marker { TestMarkerChannel, test_marker_channel_empty } +import v2.std.member_declaration_kind { DeclaredMember } import v2.std.namespace_alias { AliasBindingRow, ModuleBindingSource } // A NormalizedTree is the ADMITTED product of normalize: a root whose own lowering left no wrapper @@ -59,8 +60,17 @@ type NormalizedTree sole_constructor { import_bindings: FreeMonoid, type_declaration_kinds: FreeMonoid, type_declaration_modifiers: FreeMonoid, + member_declarations: NormalizedMemberDeclarations, } +// WHETHER THE TOP-LEVEL MEMBERS' AUTHORED KINDS WERE READ. normalize reads them from the parse +// (member_declaration_capture); a hand-built root has no parse, and an empty list would say "this module +// declares no members" about a module nothing was read for. So the unread arm is a value, never an empty +// list (v2.std.member_declaration_kind MemberKindChannel carries the same distinction forward). +type NormalizedMemberDeclarations + = MemberDeclarationsNotRead + | MemberDeclarationsRead { members: FreeMonoid } + // THE RETENTION DOOR (MQ-4). A shell the body lowering could not lower is a typed variant of its result // (v2.compiler.body_lowering_fold WrapperRetention), gathered by v2.compiler.normalize into the // BodyLoweredTree it hands here. This is where that list is CONSUMED: an empty list releases the @@ -207,13 +217,27 @@ fn admit_normalized_tree( test_markers: test_markers, import_bindings: import_bindings, type_declaration_kinds: type_declaration_kinds, - type_declaration_modifiers: type_declaration_modifiers + type_declaration_modifiers: type_declaration_modifiers, + member_declarations: MemberDeclarationsNotRead }, diagnostics: diagnostics } } } +// The one place a read member roster joins a tree, so admit_normalized_tree keeps its signature for the +// hand-built callers that hold no parse. +fn normalized_tree_with_member_declarations(tree: NormalizedTree, members: FreeMonoid) -> NormalizedTree { + NormalizedTree { + root: tree.root, + test_markers: tree.test_markers, + import_bindings: tree.import_bindings, + type_declaration_kinds: tree.type_declaration_kinds, + type_declaration_modifiers: tree.type_declaration_modifiers, + member_declarations: MemberDeclarationsRead { members: members } + } +} + fn normalized_tree_record_declarations(t: NormalizedTree) -> FreeMonoid { declared_record_names(kinds: t.type_declaration_kinds) } @@ -356,7 +380,8 @@ fn admit_unmarked_normalized_roots( test_markers: test_marker_channel_empty(), import_bindings: no_import_bindings(), type_declaration_kinds: no_type_declaration_kinds(), - type_declaration_modifiers: no_type_declaration_modifiers() + type_declaration_modifiers: no_type_declaration_modifiers(), + member_declarations: MemberDeclarationsNotRead } ) } diff --git a/src/v2/compiler/self_host/closure_emission.dag b/src/v2/compiler/self_host/closure_emission.dag index 1f14d07ab0d..13f7e9acff1 100644 --- a/src/v2/compiler/self_host/closure_emission.dag +++ b/src/v2/compiler/self_host/closure_emission.dag @@ -1,5 +1,6 @@ module v2.compiler.self_host.closure_emission +import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.compiler.tokenize { PreparedLexRules, prepare_lex_rules } import std.algebra { Cons, Empty, FreeMonoid } import std.occurrence_identity { OccurrenceIdAllocator, occurrence_id_allocator_initial, scoped_occurrence_allocator } @@ -349,7 +350,7 @@ fn closure_resolve_member( policy: default_name_resolution_policy() )), admission: Admission { subject: ResolutionSubject { name: member_module }, imports: Empty } - ).walk, symbol_index: symbol_index, closure_declarations: empty_symbol_index(), unavailable_providers: []) + ).walk, symbol_index: symbol_index, closure_declarations: empty_symbol_index(), unavailable_providers: [], member_kinds: no_member_declaration_kinds()) } ) } diff --git a/src/v2/lens/mandatory_tag.dag b/src/v2/lens/mandatory_tag.dag index 39a71909c61..1f798fcae49 100644 --- a/src/v2/lens/mandatory_tag.dag +++ b/src/v2/lens/mandatory_tag.dag @@ -25,10 +25,36 @@ import v2.std.diagnostic { node_locus, outcome_accepted } -import v2.std.node { Atom, Edge, Node, NodeFold, Symbol, TypeNode, fold_node } +import v2.std.node { + ArrowBodyEdge, + Atom, + Authored, + ComputationNode, + StructuralLabel, + Edge, + Node, + NodeFold, + Positional, + Symbol, + TypeNode, + core_edge_label, + fold_node, + node_is_arrow +} import v2.std.node_query { find_named_child } import v2.std.qualified_name { QualifiedName, qualified_name_to_dotted_string } import v2.std.text { String } +import v2.compiler.namespace_graft { namespace_graft_module_body_optional } +import v2.std.member_declaration_kind { + DeclaredDataMember, + DeclaredFnMember, + MemberKindChannel, + MemberKindDeclared, + MemberKindNotDeclared, + MemberKindProvenanceUnavailable, + member_kind_lookup, + no_member_declaration_kinds +} import v2.std.witness { Holds, Witness } import v2.std.grammar { node_atom_identity_optional } import v2.extdeps.languages.dag { @@ -75,13 +101,12 @@ import v2.extdeps.languages.dag { // non-external, the old NonExternalAnchorScheme refusal). The tagged declaration's value subtree is // scanned for vocabulary atoms: any non-accepted atom refuses; none found refuses IF the value // region structurally carries its expression content (dag_surface_expr productions present - -// parse-shaped and emit-shaped trees), and is out of representation IF the region carries no -// expression productions (03_normalize currently collapses data-decl value internals to bare token -// markers - the general-body-producer frontier, docs/plans/general-body-producer-design.md). The -// out-of-representation arm contributes no finding at THIS grain because the fact is absent from -// the carrier, not because the check widened - the corpus witness enforces the same rule at parse -// grain, where value content is always present, so scheme enforcement stays whole-corpus while the -// normalize-grain representation matures. +// parse-shaped and emit-shaped trees) and when the declaration is a lowered Arrow member, whose +// initializer body is its value content. A tree whose declaration carries neither is out of +// representation and contributes no finding, because the fact is absent from the carrier, not +// because the check widened. Since normalize lowers a data declaration to a named Arrow +// (body_lower_data_decl_to_member) the normalized and inferred grains carry the value, so scheme +// enforcement holds there too (see the lowered carrier shape beside mandatory_tag_decl_type_node). type MandatoryTagRegion { region_dotted_prefix: String @@ -284,18 +309,83 @@ fn mandatory_tag_decl_name(d: Node) -> MandatoryTagDeclName { } } +// THE LOWERED CARRIER SHAPE. Normalize lowers a `data` declaration to a named nullary Arrow member +// (v2.compiler.body_lowering_fold body_lower_data_decl_to_member, 2026-09-24, #12197): the +// dag_surface_data_decl production is consumed and the declaration stands as a Conj member whose +// Authored edge carries the declared name and targets an Arrow whose domain is the first Positional +// child, whose codomain is the second (body_lower_callable_arrow), and whose initializer is the +// ArrowBodyEdge target. The root lens grain runs over the inferred tree, so this is the shape the +// compile door actually hands this gate; a reader of only the parse and emit shapes finds no +// declaration and reports every well-tagged module as missing its tag. +type MandatoryTagPositionalScan { + seen: Int + second: Optional +} + +fn mandatory_tag_lowered_codomain(d: Node) -> Optional { + let scan = fold(d.children, init: MandatoryTagPositionalScan { seen: 0, second: optional_absent() }, f: fn(acc, e) { + match e.label { + Positional => + MandatoryTagPositionalScan { + seen: acc.seen + 1, + second: if acc.seen == 1 { optional_present(value: e.target) } else { acc.second } + } + Authored { name: _ } => acc + StructuralLabel { label: _ } => acc + } + }) + scan.second +} + +fn mandatory_tag_lowered_body(d: Node) -> Optional { + fold(d.children, init: optional_absent(), f: fn(acc, e) { + if e.label == core_edge_label(marker: ArrowBodyEdge) { optional_present(value: e.target) } else { acc } + }) +} + +// A DIRECT top-level member of the module body: an Authored edge on the grafted module body (never a +// descendant of a member, so a nested Arrow-valued member of the same name is not it) whose target is an +// Arrow. That a lowered Arrow is a DATA declaration is not readable here -- a zero-argument fn lowers to the +// same shape -- so this finds the candidate and the member-kind channel decides what it is. +fn mandatory_tag_lowered_member(module_node: Node, required_name: Symbol) -> Optional { + match namespace_graft_module_body_optional(root: module_node) { + Absent => optional_absent() + Present { value: body } => + fold(body.children, init: optional_absent(), f: fn(acc, e) { + match e.label { + Authored { name: nm } => + if (nm == required_name) && node_is_arrow(n: e.target) { + optional_present(value: e.target) + } else { + acc + } + StructuralLabel { label: _ } => acc + Positional => acc + } + }) + } +} + fn mandatory_tag_decl_type_node(d: Node) -> Optional { + if node_is_arrow(n: d) { + mandatory_tag_lowered_codomain(d: d) + } else { match find_named_child(root: d, name: ^dag_surface_data_decl_type) { Accepted { value: ty, diagnostics: _ } => optional_present(value: ty) Rejected { diagnostics: _ } => mandatory_tag_parse_type_node(d: d) } + } } fn mandatory_tag_decl_value_node(d: Node) -> Optional { + if node_is_arrow(n: d) { + mandatory_tag_lowered_body(d: d) + } else { match find_named_child(root: d, name: ^dag_surface_data_decl_expr) { Accepted { value: v, diagnostics: _ } => optional_present(value: v) Rejected { diagnostics: _ } => mandatory_tag_parse_value_node(d: d) } + } } type MandatoryTagDeclScan { @@ -340,6 +430,14 @@ fn mandatory_tag_missing_decl_diagnostic(module_node: Node) -> Diagnostic { } } +fn mandatory_tag_member_provenance_unavailable_diagnostic(module_node: Node) -> Diagnostic { + Diagnostic { + reason: ^mandatory_tag_member_provenance_unavailable, + at: node_locus(node: module_node), + correction: Unavailable { reason: ExternalContractUnknown } + } +} + fn mandatory_tag_projection_gated_diagnostic(module_node: Node) -> Diagnostic { Diagnostic { reason: ^mandatory_tag_name_projection_gated, @@ -407,7 +505,7 @@ fn mandatory_tag_value_findings(d: Node, region: MandatoryTagRegion) -> List - if mandatory_tag_subtree_has_production(n: v, want: ^dag_surface_expr) { + if node_is_arrow(n: d) || mandatory_tag_subtree_has_production(n: v, want: ^dag_surface_expr) { [mandatory_tag_value_unreadable_diagnostic(d: d)] } else { [] @@ -426,10 +524,45 @@ fn mandatory_tag_value_findings(d: Node, region: MandatoryTagRegion) -> List List { + match member_kind_lookup(channel: channel, module: dotted, name: region.required_decl_name) { + MemberKindProvenanceUnavailable => [mandatory_tag_member_provenance_unavailable_diagnostic(module_node: module_node)] + MemberKindNotDeclared => [mandatory_tag_missing_decl_diagnostic(module_node: module_node)] + MemberKindDeclared { kind: kind } => + match kind { + DeclaredFnMember => [mandatory_tag_missing_decl_diagnostic(module_node: module_node)] + DeclaredDataMember => + match mandatory_tag_lowered_codomain(d: candidate) { + Absent => [mandatory_tag_type_mismatch_diagnostic(d: candidate)] + Present { value: _ } => + match mandatory_tag_lowered_body(d: candidate) { + Absent => [mandatory_tag_value_unreadable_diagnostic(d: candidate)] + Present { value: _ } => + concat( + mandatory_tag_type_findings(d: candidate, region: region), + mandatory_tag_value_findings(d: candidate, region: region) + ) + } + } + } + } +} + fn mandatory_tag_region_module_findings( region: MandatoryTagRegion, module_node: Node, - dotted: String + dotted: String, + channel: MemberKindChannel ) -> List { if mandatory_tag_region_applies(region: region, dotted: dotted) { let scan = mandatory_tag_scan_decls( @@ -444,7 +577,17 @@ fn mandatory_tag_region_module_findings( ) Absent => if scan.projection_gated_count == 0 { - [mandatory_tag_missing_decl_diagnostic(module_node: module_node)] + match mandatory_tag_lowered_member(module_node: module_node, required_name: region.required_decl_name) { + Absent => [mandatory_tag_missing_decl_diagnostic(module_node: module_node)] + Present { value: candidate } => + mandatory_tag_lowered_candidate_findings( + region: region, + module_node: module_node, + dotted: dotted, + candidate: candidate, + channel: channel + ) + } } else { [mandatory_tag_projection_gated_diagnostic(module_node: module_node)] } @@ -454,7 +597,7 @@ fn mandatory_tag_region_module_findings( } } -fn mandatory_tag_module_findings(n: Node) -> List { +fn mandatory_tag_module_findings(n: Node, channel: MemberKindChannel) -> List { if mandatory_tag_node_production_is(n: n, want: ^dag_surface_module) { match qualified_name_from_module_node(root: n) { Rejected { diagnostics: _ } => [] @@ -466,7 +609,8 @@ fn mandatory_tag_module_findings(n: Node) -> List { mandatory_tag_region_module_findings( region: region, module_node: n, - dotted: dotted + dotted: dotted, + channel: channel ) ) }) @@ -481,22 +625,32 @@ fn mandatory_tag_module_findings(n: Node) -> List { // malformed module headers upstream of every root lens, so the nameless-wrapper arm is unreachable // on a tree that reached the lens roster; keying region membership on a fabricated name would be // the fabricated-plausible-output trap the arm avoids. -fn mandatory_tag_findings(root: Node) -> List { +fn mandatory_tag_findings_with_provenance(root: Node, channel: MemberKindChannel) -> List { fold_node( n: root, algebra: NodeFold { - init: fn(n0) { mandatory_tag_module_findings(n: n0) }, + init: fn(n0) { mandatory_tag_module_findings(n: n0, channel: channel) }, step: fn(acc, _edge, child) { concat(acc, child) } } ) } +// The parse/emit grain: no provenance is read, so a lowered candidate refuses as provenance-unavailable. +fn mandatory_tag_findings(root: Node) -> List { + mandatory_tag_findings_with_provenance(root: root, channel: no_member_declaration_kinds()) +} + fn mandatory_tag_findings_count(root: Node) -> Int { length(xs: mandatory_tag_findings(root: root)) } fn mandatory_tag_compile_gate(node: Node) -> Outcome> { - match mandatory_tag_findings(root: node) { + mandatory_tag_compile_gate_with_provenance(node: node, channel: no_member_declaration_kinds()) +} + +// The compile door's entry: the channel is the member-kind provenance ResolvedTree carries for this subject. +fn mandatory_tag_compile_gate_with_provenance(node: Node, channel: MemberKindChannel) -> Outcome> { + match mandatory_tag_findings_with_provenance(root: node, channel: channel) { Cons { head: first, tail: rest } => Rejected { diagnostics: NonEmptyDiagnostics { head: first, tail: rest } diff --git a/src/v2/std/member_declaration_kind.dag b/src/v2/std/member_declaration_kind.dag new file mode 100644 index 00000000000..cd332a3a74b --- /dev/null +++ b/src/v2/std/member_declaration_kind.dag @@ -0,0 +1,105 @@ +module v2.std.member_declaration_kind + +import std.types { List } +import std.algebra { FreeMonoid } +import v2.std.algebra { fold_list } +import v2.std.collection { Map, empty_map, map_contains_key, map_insert } +import v2.std.integer { Int } +import v2.std.node { Symbol } +import v2.std.qualified_name { QualifiedName, qualified_name_to_dotted_string } +import v2.std.text { String } + +// WHICH KIND OF DECLARATION AUTHORED EACH TOP-LEVEL MEMBER, carried because lowering erases it. +// Normalize lowers a `data` declaration to a named nullary Arrow member +// (v2.compiler.body_lowering_fold body_lower_data_decl_to_member) whose shape is, by design, +// identical to a zero-argument `fn` lowered by body_lower_fn_decl_to_arrow: both are a Conj member +// whose Authored edge names an Arrow with an empty domain, a codomain and a body. After lowering no +// reader of the Node can tell `data x: T = v` from `fn x() -> T { v }`, so a reader that must hold +// the first and refuse the second has nothing to read, and classifying a generic Arrow as a data +// declaration is the impersonation hole. The fact is read where it still exists -- on the parse, at +// the one capture site of v2.compiler.normalize -- exactly as type_declaration_kinds is, sealed on +// NormalizedTree beside the root rather than as a structural child edge (which would change the +// content hash of every data declaration), and handed forward by the caller that holds it. +type MemberDeclarationKind + = DeclaredDataMember + | DeclaredFnMember + +// A top-level member by its authored name and kind, as read from ONE module's parse. Unqualified: +// the module that declares it is the NormalizedTree it rides on. +type DeclaredMember { + name: Symbol + kind: MemberDeclarationKind +} + +// A member by its DECLARING path -- the module's qualified name and the member's own name, never a +// bare spelling, because .dag member names are corpus-global (the way symbol_index_fill qualifies). +type QualifiedDeclaredMember { + module: QualifiedName + name: Symbol + kind: MemberDeclarationKind +} + +// THE CHANNEL A LATER-GRAIN CONSUMER RECEIVES. It names the modules it COVERS, because an empty member +// list is ambiguous between "this module declares no such member" and "nothing was read": the first is +// a fact, the second is the absence of one, and a consumer that reads the second as the first refuses +// every module (a false absence) while one that reads it as "fine" accepts every module (a fabricated +// pass). MemberKindsUnavailable is the explicit second arm, so a constructor site that holds no parse +// says so by value (no_member_declaration_kinds), like no_type_declaration_kinds. +type MemberKindChannel + = MemberKindsUnavailable + | MemberKindsCaptured { covered: List, members: List } + +fn no_member_declaration_kinds() -> MemberKindChannel { + MemberKindsUnavailable +} + +type MemberKindLookup + = MemberKindProvenanceUnavailable + | MemberKindNotDeclared + | MemberKindDeclared { kind: MemberDeclarationKind } + +fn member_kind_module_is(module: QualifiedName, wanted: String) -> Bool { + qualified_name_to_dotted_string(qn: module) == wanted +} + +// The kind the channel records for `name` declared at the top level of the module whose dotted name is +// `module`. Unavailable when the channel was never read OR does not cover that module: both mean the +// provenance is not there, and neither may answer "not declared". +fn member_kind_lookup(channel: MemberKindChannel, module: String, name: Symbol) -> MemberKindLookup { + match channel { + MemberKindsUnavailable => MemberKindProvenanceUnavailable + MemberKindsCaptured { covered: covered, members: members } => + if fold(covered, init: false, f: fn(acc, m) { acc || member_kind_module_is(module: m, wanted: module) }) { + fold(members, init: MemberKindNotDeclared, f: fn(acc, m) { + if member_kind_module_is(module: m.module, wanted: module) && (m.name == name) { + MemberKindDeclared { kind: m.kind } + } else { + acc + } + }) + } else { + MemberKindProvenanceUnavailable + } + } +} + +// Two members of one module sharing a name is a duplicate declaration whatever their kinds (a data and a fn of +// one name conflict as surely as two of one kind); the channel refuses it, never first-wins. ONE PASS: the names +// seen so far ride a map, so each member costs one membership probe instead of a rescan of the list. +type MemberNamesSeen { + seen: Map + duplicate: Bool +} + +fn declared_members_have_duplicate(members: FreeMonoid) -> Bool { + fold_list( + xs: members, + empty: MemberNamesSeen { seen: empty_map(), duplicate: false }, + cons: fn(acc, m) { + MemberNamesSeen { + seen: map_insert(m: acc.seen, key: m.name, value: true), + duplicate: acc.duplicate || map_contains_key(m: acc.seen, key: m.name) + } + } + ).duplicate +} diff --git a/src/v2/std/node.dag b/src/v2/std/node.dag index 28e9f79bdeb..e40efe9e58c 100644 --- a/src/v2/std/node.dag +++ b/src/v2/std/node.dag @@ -309,6 +309,16 @@ fn node_with_occurrence_id( Node { kind: kind, children: children, occurrence_id: occurrence_id } } +// Whether the node is an Arrow type node -- the one connective question every reader of a lowered callable or +// nullary-member shape asks. Single accessor: readers import this rather than re-matching the coproduct. +fn node_is_arrow(n: Node) -> Bool { + match n.kind { + TypeNode { connective: Arrow } => true + TypeNode { connective: _ } => false + ComputationNode { behavior: _ } => false + } +} + fn node_rebuild(n: Node, children: List) -> Node { node_with_occurrence_id( kind: n.kind, diff --git a/src/v2/test/claim/arrow_order_edge/admission_wall_test.dag b/src/v2/test/claim/arrow_order_edge/admission_wall_test.dag index d16fc6f172b..55a8e49ba39 100644 --- a/src/v2/test/claim/arrow_order_edge/admission_wall_test.dag +++ b/src/v2/test/claim/arrow_order_edge/admission_wall_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.arrow_order_edge.admission_wall +import v2.std.member_declaration_kind { no_member_declaration_kinds } import std.occurrence_identity { OccurrenceSynthetic } import std.algebra { Cons, Empty } import v2.compiler.infer { infer } @@ -81,7 +82,7 @@ test fn aoe_well_formed_refuses_a_named_domain_without_order() -> Bool { // PATH: infer, entered directly with a ResolvedTree. fn aoe_infer_reason(arrow: Node) -> Symbol { - match infer(tree: ResolvedTree { root: aoe_module_root(arrow: arrow), symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] }) { + match infer(tree: ResolvedTree { root: aoe_module_root(arrow: arrow), symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() }) { Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) Accepted { value: _, diagnostics: _ } => ^aoe_accepted } diff --git a/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag b/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag index dae2c75a68b..d1e9c465b02 100644 --- a/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag +++ b/src/v2/test/claim/compiler/infer_fold_member_instance_test.dag @@ -208,7 +208,8 @@ fn fmi_infer_with_member_formal_authored(tree: ResolvedTree) -> Outcome { symbol_index: tree.symbol_index, resolved_declarations: tree.resolved_declarations, lexical_bindings: tree.lexical_bindings, - unavailable_providers: tree.unavailable_providers + unavailable_providers: tree.unavailable_providers, + member_kinds: tree.member_kinds }) { Rejected { diagnostics: d } => Rejected { diagnostics: d } Accepted { value: _, diagnostics: d } => Accepted { value: true, diagnostics: d } diff --git a/src/v2/test/claim/compiler/infer_record_construct_field_inhabitance_witness_test.dag b/src/v2/test/claim/compiler/infer_record_construct_field_inhabitance_witness_test.dag index d9c43a793a3..7cc4f0fac10 100644 --- a/src/v2/test/claim/compiler/infer_record_construct_field_inhabitance_witness_test.dag +++ b/src/v2/test/claim/compiler/infer_record_construct_field_inhabitance_witness_test.dag @@ -299,7 +299,7 @@ fn rcf_member_accepted_and_decided(resolved: Outcome, member: Symb match rcf_member_arrow(root: tree.root, name: member) { Absent => false Present { value: arrow } => - match infer(tree: ResolvedTree { root: arrow, symbol_index: tree.symbol_index, resolved_declarations: tree.resolved_declarations, lexical_bindings: tree.lexical_bindings, unavailable_providers: tree.unavailable_providers }) { + match infer(tree: ResolvedTree { root: arrow, symbol_index: tree.symbol_index, resolved_declarations: tree.resolved_declarations, lexical_bindings: tree.lexical_bindings, unavailable_providers: tree.unavailable_providers, member_kinds: tree.member_kinds }) { Rejected { diagnostics: _ } => false Accepted { value: _, diagnostics: ds } => !diagnostics_has_reason(d: ds, reason: ^inhabitance_undecidable_formal_unresolved) diff --git a/src/v2/test/claim/compiler/kernel_value_type_roster_witness_test.dag b/src/v2/test/claim/compiler/kernel_value_type_roster_witness_test.dag index 8df7137c1ea..161eb4b8994 100644 --- a/src/v2/test/claim/compiler/kernel_value_type_roster_witness_test.dag +++ b/src/v2/test/claim/compiler/kernel_value_type_roster_witness_test.dag @@ -200,7 +200,7 @@ test fn kvr_a_named_calls_bool_formal_holding_an_int_refuses_holds() -> Bool { match rcf_member_arrow(root: tree.root, name: ^kvr_g) { Absent => false Present { value: arrow } => - match infer(tree: ResolvedTree { root: arrow, symbol_index: tree.symbol_index, resolved_declarations: tree.resolved_declarations, lexical_bindings: tree.lexical_bindings, unavailable_providers: tree.unavailable_providers }) { + match infer(tree: ResolvedTree { root: arrow, symbol_index: tree.symbol_index, resolved_declarations: tree.resolved_declarations, lexical_bindings: tree.lexical_bindings, unavailable_providers: tree.unavailable_providers, member_kinds: tree.member_kinds }) { Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^application_argument_does_not_inhabit Accepted { value: _, diagnostics: _ } => false } diff --git a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag index 976bf823584..f63f6434c8f 100644 --- a/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag +++ b/src/v2/test/claim/execution/long/emit_host_classical_not_ingested_equals_eval_test.dag @@ -1,5 +1,6 @@ module v2.test.long.emit_host_classical_not_ingested_equals_eval +import v2.std.member_declaration_kind { no_member_declaration_kinds } import std.types { List } import v2.compiler.refinement_discharge { infer_and_discharge } import std.occurrence_identity { OccurrenceSynthetic } @@ -148,7 +149,7 @@ fn ingested_arrow_from_source(source: String) -> Outcome { f: fn(resolved) { match ingested_find_arrow_in_module(root: resolved.root) { Present { value: arrow } => - outcome_accepted(value: ResolvedTree { root: arrow, symbol_index: empty_symbol_index(), resolved_declarations: resolved.resolved_declarations, lexical_bindings: resolved.lexical_bindings, unavailable_providers: resolved.unavailable_providers }) + outcome_accepted(value: ResolvedTree { root: arrow, symbol_index: empty_symbol_index(), resolved_declarations: resolved.resolved_declarations, lexical_bindings: resolved.lexical_bindings, unavailable_providers: resolved.unavailable_providers, member_kinds: no_member_declaration_kinds() }) Absent => outcome_rejected( d: ingested_classical_not_diagnostic(reason: ^ingested_classical_not_arrow_miss, node: resolved.root) diff --git a/src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag b/src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag index 46339204fa7..cf9e6043703 100644 --- a/src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag +++ b/src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag @@ -7,7 +7,10 @@ import v2.compiler.normalize { normalize } import v2.compiler.compile { CompileLens, CompileLensRoot, required_lenses_at_grain } import v2.compiler.infer { InferredTree } import v2.extdeps.languages.dag { dag_language_model } -import v2.lens.mandatory_tag { mandatory_tag_compile_gate } +import v2.lens.mandatory_tag { mandatory_tag_compile_gate_with_provenance } +import v2.compiler.resolve { member_kind_channel_of_tree } +import v2.std.member_declaration_kind { MemberKindChannel } +import v2.compiler.namespace_graft { namespace_graft_build_body_conj, namespace_graft_fold_spine, namespace_graft_wrap_module_shell } import std.algebra { Cons, Empty } import v2.std.collection { empty_map} import v2.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } @@ -27,12 +30,16 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // fast-lane eval budget - discovery excludes test/claim/long/ at dir grain and the run-29892063728 // receipt shows all 12 witnesses EvalBudgetExceeded in place. Recipe: claim_batch --source-root // src/v2 --source-root dag --entry src/v2/test/claim/long/mandatory_tag_gate_witness_test.dag -// --functions --claim-run --wet (~2min; run receipted green 2026-07-22, +// --functions --claim-run --wet (~2min; run receipted green 2026-07-22, // 12/12 PASS). Parse grain carries the full declaration (name lexeme, type annotation, value // vocabulary), so every arm is exercised there, including the misnamed-anchor control - the exact -// #6991 regression class this wall makes unwritable. Normalize grain currently collapses data-decl -// value internals (general-body-producer frontier), so its controls cover name/type/missing only; -// scheme enforcement at corpus scale rides the parse-grain corpus witness. The roster control +// #6991 regression class this wall makes unwritable. Normalize grain lowers a data declaration to a named +// nullary Arrow member (body_lower_data_decl_to_member, #12197, 2026-09-24), which the gate reads +// for name, type and value; the normalized controls cover clean/missing/misnamed (the wrong-type, +// file-scheme and bogus-scheme reds at this grain were measured and each exceeds the new-witness +// eval-step budget, so they are not enrolled; parse grain carries those arms). Regression receipt: the 2026-07-22 12/12 run predates that +// lowering, after which the gate read no declaration at this grain and reported every tagged module +// missing (eea7e8ea86); scheme enforcement at corpus scale rides the parse-grain corpus witness. The roster control // proves enrollment by execution: a violating module tree pushed through every enrolled root lens // yields a rejection whose head reason is mandatory_tag_missing_required_decl - a reason only this // lens emits. @@ -55,7 +62,7 @@ data src_exempt_fixture: String = "module extdeps.fixture.gate_probe_planted\n\n type GrainProbe = GrainStageRejected - | GrainTree { root: Node } + | GrainTree { root: Node, channel: MemberKindChannel } fn parse_grain_tree(source: String) -> GrainProbe { let lm = dag_language_model() @@ -64,7 +71,7 @@ fn parse_grain_tree(source: String) -> GrainProbe { Accepted { value: ts, diagnostics: _ } => match parse_module(tokens: ts, grammar: lm.grammar) { Rejected { diagnostics: _ } => GrainStageRejected - Accepted { value: artifact, diagnostics: _ } => GrainTree { root: artifact.tree } + Accepted { value: artifact, diagnostics: _ } => GrainTree { root: artifact.tree, channel: no_member_declaration_kinds() } } } } @@ -75,7 +82,11 @@ fn normalized_grain_tree(source: String) -> GrainProbe { GrainTree { root: parse_root } => match normalize(parse_tree: parse_root) { Rejected { diagnostics: _ } => GrainStageRejected - Accepted { value: normalized, diagnostics: _ } => GrainTree { root: normalized.root } + Accepted { value: normalized, diagnostics: _ } => + match member_kind_channel_of_tree(tree: normalized) { + Rejected { diagnostics: _ } => GrainStageRejected + Accepted { value: channel, diagnostics: _ } => GrainTree { root: normalized.root, channel: channel } + } } } } @@ -83,8 +94,8 @@ fn normalized_grain_tree(source: String) -> GrainProbe { fn gate_accepts_tree(probe: GrainProbe) -> Bool { match probe { GrainStageRejected => false - GrainTree { root: root } => - match mandatory_tag_compile_gate(node: root) { + GrainTree { root: root, channel: channel } => + match mandatory_tag_compile_gate_with_provenance(node: root, channel: channel) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } @@ -94,8 +105,8 @@ fn gate_accepts_tree(probe: GrainProbe) -> Bool { fn gate_rejects_tree_with(probe: GrainProbe, reason: Symbol) -> Bool { match probe { GrainStageRejected => false - GrainTree { root: root } => - match mandatory_tag_compile_gate(node: root) { + GrainTree { root: root, channel: channel } => + match mandatory_tag_compile_gate_with_provenance(node: root, channel: channel) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: d } => if d.head.reason == reason { @@ -175,7 +186,7 @@ test fn mandatory_tag_normalized_grain_misnamed_rejects() -> Bool { fn roster_rejects_with(probe: GrainProbe, reason: Symbol) -> Bool { match probe { GrainStageRejected => false - GrainTree { root: root } => + GrainTree { root: root, channel: _ } => let inferred = InferredTree { root: root, facts: empty_map() } fold(required_lenses_at_grain(grain: CompileLensRoot), init: false, f: fn(acc, lens) { acc diff --git a/src/v2/test/claim/mandatory_tag_supplied_carrier_witness_test.dag b/src/v2/test/claim/mandatory_tag_supplied_carrier_witness_test.dag new file mode 100644 index 00000000000..4b0b12c0965 --- /dev/null +++ b/src/v2/test/claim/mandatory_tag_supplied_carrier_witness_test.dag @@ -0,0 +1,285 @@ +module v2.test.claim.mandatory_tag_supplied_carrier_witness + +import std.types { List } +import v2.lens.mandatory_tag { mandatory_tag_compile_gate_with_provenance, mandatory_tag_lowered_candidate_findings, extdeps_external_authority_region } +import v2.compiler.namespace_graft { namespace_graft_build_body_conj, namespace_graft_fold_spine, namespace_graft_wrap_module_shell } +import v2.std.member_declaration_kind { + DeclaredDataMember, + DeclaredFnMember, + DeclaredMember, + MemberKindChannel, + MemberKindsCaptured, + QualifiedDeclaredMember, + declared_members_have_duplicate, + no_member_declaration_kinds +} +import v2.std.qualified_name { QualifiedName } +import std.occurrence_identity { OccurrenceSynthetic } +import v2.std.node { Arrow, Authored, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } +import std.algebra { Cons, Empty } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.integer { Int } +import v2.std.node { Symbol } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// FAST-LANE supplied-carrier controls for the mandatory-tag gate's lowered-member path (DESIGN section 3: a +// witness discriminates at ONE interface, its inputs supplied rather than derived). No tokenize, parse or +// normalize runs: the candidate Arrow, the grafted module and the member-kind channel are built values, so each +// control costs a few hundred to ~2k eval steps and is selected by the required floor. The real route +// (normalize -> captured member channel -> member_kind_channel_of_tree -> mandatory_tag_compile_gate_with_provenance) +// is the pairing inhabitance claim in v2.test.long.mandatory_tag_gate_witness +// (mandatory_tag_normalized_grain_clean_accepts); NOT executed by any claim: resolve_in_context -> +// ResolvedTree.member_kinds -> validate_then_compile rebinding (gunbc.guarantee_stall +// member_kind_door_binding_executed_by_no_claim_stall). + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +type GateProbe { root: Node channel: MemberKindChannel } + +fn gate_accepts_tree(probe: GateProbe) -> Bool { + match mandatory_tag_compile_gate_with_provenance(node: probe.root, channel: probe.channel) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +fn gate_rejects_tree_with(probe: GateProbe, reason: Symbol) -> Bool { + match mandatory_tag_compile_gate_with_provenance(node: probe.root, channel: probe.channel) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: d } => + if d.head.reason == reason { + true + } else { + fold(d.tail, init: false, f: fn(acc, diag) { acc || diag.reason == reason }) + } + } +} + +// SUPPLIED-CARRIER CONTROLS at the lens's own interface (DESIGN section 3, a witness discriminates at one +// interface): the candidate Arrow and the member-kind channel are supplied values, so no frontend runs. The +// real route is executed only as far as: normalize -> captured member channel -> member_kind_channel_of_tree -> +// mandatory_tag_compile_gate_with_provenance (mandatory_tag_normalized_grain_clean_accepts above; deleting that +// integration makes it fail). NOT executed by any claim: resolve_in_context -> ResolvedTree.member_kinds -> +// validate_then_compile rebinding; that link is the standing GuaranteeStall +// gunbc.guarantee_stall member_kind_door_binding_executed_by_no_claim_stall. +fn mt_atom(s: Symbol) -> Node { + Node { kind: TypeNode { connective: Atom { identity: s } }, children: [], occurrence_id: OccurrenceSynthetic } +} + +fn mt_domain() -> Node { + Node { kind: TypeNode { connective: Conj }, children: [], occurrence_id: OccurrenceSynthetic } +} + +fn mt_candidate(codomain: Symbol, body: List) -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [ + Edge { label: Positional, target: mt_domain() }, + Edge { label: Positional, target: mt_atom(s: codomain) }, + Edge { label: core_edge_label(marker: ArrowBodyEdge), target: mt_body(atoms: body) } + ], + occurrence_id: OccurrenceSynthetic + } +} + +fn mt_body(atoms: List) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: fold(atoms, init: [], f: fn(acc, a) { concat(acc, [Edge { label: Positional, target: mt_atom(s: a) }]) }), + occurrence_id: OccurrenceSynthetic + } +} + +fn mt_no_codomain() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [Edge { label: Positional, target: mt_domain() }, Edge { label: core_edge_label(marker: ArrowBodyEdge), target: mt_body(atoms: [^Https]) }], + occurrence_id: OccurrenceSynthetic + } +} + +fn mt_no_body() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [Edge { label: Positional, target: mt_domain() }, Edge { label: Positional, target: mt_atom(s: ^ExternalAuthority) }], + occurrence_id: OccurrenceSynthetic + } +} + +fn mt_channel(kind: MemberKindChannel) -> MemberKindChannel { + kind +} + +fn mt_captured(kind: MemberKindDeclaredFor) -> MemberKindChannel { + MemberKindsCaptured { + covered: [mt_module()], + members: mt_members(kind: kind) + } +} + +type MemberKindDeclaredFor + = ForData + | ForFn + | ForNothing + +fn mt_module() -> QualifiedName { + [^extdeps, ^gate_probe_supplied] +} + +fn mt_members(kind: MemberKindDeclaredFor) -> List { + match kind { + ForData => [QualifiedDeclaredMember { module: mt_module(), name: ^extdeps_external_authority_anchor, kind: DeclaredDataMember }] + ForFn => [QualifiedDeclaredMember { module: mt_module(), name: ^extdeps_external_authority_anchor, kind: DeclaredFnMember }] + ForNothing => [] + } +} + +fn mt_findings(candidate: Node, channel: MemberKindChannel) -> List { + fold( + mandatory_tag_lowered_candidate_findings( + region: extdeps_external_authority_region, + module_node: candidate, + dotted: "extdeps.gate_probe_supplied", + candidate: candidate, + channel: channel + ), + init: [], + f: fn(acc, d) { concat(acc, [d.reason]) } + ) +} + +fn mt_only(candidate: Node, channel: MemberKindChannel, reason: Symbol) -> Bool { + match mt_findings(candidate: candidate, channel: channel) { + Cons { head: h, tail: Empty } => h == reason + Cons { head: _, tail: Cons { head: _, tail: _ } } => false + Empty => false + } +} + +// TOP-LEVEL SELECTOR, SUPPLIED-CARRIER GRAIN: the grafted module is built directly (no parse, no normalize) by the +// graft's own constructors. Its one DIRECT member is unrelated; the required name appears only NESTED inside that +// member's Arrow as a valid Arrow, and the channel would admit that name as a data member. Must refuse as missing. +fn mt_unrelated_member_nesting_anchor() -> Node { + Node { + kind: TypeNode { connective: Arrow }, + children: [ + Edge { label: Positional, target: mt_domain() }, + Edge { label: Positional, target: mt_atom(s: ^Int) }, + Edge { label: Authored { name: ^extdeps_external_authority_anchor }, target: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]) } + ], + occurrence_id: OccurrenceSynthetic + } +} + +fn mt_nested_anchor_module() -> Node { + namespace_graft_wrap_module_shell(captured: mt_nested_anchor_spine(), source: mt_domain()) +} + +fn mt_nested_anchor_spine() -> Node { + mt_spine_with(edges: [Edge { label: Authored { name: ^gate_probe_unrelated_row }, target: mt_unrelated_member_nesting_anchor() }]) +} + +fn mt_direct_anchor_module() -> Node { + namespace_graft_wrap_module_shell( + captured: mt_spine_with(edges: [Edge { label: Authored { name: ^extdeps_external_authority_anchor }, target: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]) }]), + source: mt_domain() + ) +} + +fn mt_spine_with(edges: List) -> Node { + namespace_graft_fold_spine( + qn: mt_module(), + body: namespace_graft_build_body_conj( + edges: edges, + source: mt_domain() + ), + source: mt_domain() + ) +} + +test fn mandatory_tag_supplied_nested_anchor_under_unrelated_member_refuses_as_missing() -> Bool { + gate_rejects_tree_with( + probe: GateProbe { root: mt_nested_anchor_module(), channel: mt_captured(kind: ForData) }, + reason: ^mandatory_tag_missing_required_decl + ) +} + +test fn mandatory_tag_supplied_direct_anchor_member_in_grafted_module_accepts() -> Bool { + gate_accepts_tree(probe: GateProbe { root: mt_direct_anchor_module(), channel: mt_captured(kind: ForData) }) +} + +test fn mandatory_tag_supplied_data_member_with_good_carrier_accepts() -> Bool { + match mt_findings(candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]), channel: mt_captured(kind: ForData)) { + Empty => true + Cons { head: _, tail: _ } => false + } +} + +test fn mandatory_tag_supplied_zero_arg_fn_same_shape_refuses_as_missing() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]), + channel: mt_captured(kind: ForFn), + reason: ^mandatory_tag_missing_required_decl + ) +} + +test fn mandatory_tag_supplied_member_not_declared_refuses_as_missing() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]), + channel: mt_captured(kind: ForNothing), + reason: ^mandatory_tag_missing_required_decl + ) +} + +test fn mandatory_tag_supplied_unread_provenance_refuses_as_unavailable() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]), + channel: no_member_declaration_kinds(), + reason: ^mandatory_tag_member_provenance_unavailable + ) +} + +test fn mandatory_tag_supplied_uncovered_module_refuses_as_unavailable() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]), + channel: MemberKindsCaptured { covered: [[^extdeps, ^some_other_module]], members: [] }, + reason: ^mandatory_tag_member_provenance_unavailable + ) +} + +test fn mandatory_tag_supplied_wrong_codomain_refuses_as_type_mismatch() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^SomethingElse, body: [^Https]), + channel: mt_captured(kind: ForData), + reason: ^mandatory_tag_required_decl_type_mismatch + ) +} + +test fn mandatory_tag_supplied_missing_codomain_or_body_refuses() -> Bool { + mt_only(candidate: mt_no_codomain(), channel: mt_captured(kind: ForData), reason: ^mandatory_tag_required_decl_type_mismatch) + && mt_only(candidate: mt_no_body(), channel: mt_captured(kind: ForData), reason: ^mandatory_tag_value_vocabulary_unreadable) +} + +test fn mandatory_tag_supplied_wrong_or_missing_vocabulary_atom_refuses() -> Bool { + mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: [^File]), + channel: mt_captured(kind: ForData), + reason: ^mandatory_tag_value_not_accepted + ) + && mt_only( + candidate: mt_candidate(codomain: ^ExternalAuthority, body: []), + channel: mt_captured(kind: ForData), + reason: ^mandatory_tag_value_vocabulary_unreadable + ) +} + +test fn member_kind_channel_duplicate_declaration_is_detected() -> Bool { + declared_members_have_duplicate(members: [ + DeclaredMember { name: ^extdeps_external_authority_anchor, kind: DeclaredDataMember }, + DeclaredMember { name: ^extdeps_external_authority_anchor, kind: DeclaredFnMember } + ]) + && !declared_members_have_duplicate(members: [ + DeclaredMember { name: ^extdeps_external_authority_anchor, kind: DeclaredDataMember }, + DeclaredMember { name: ^other_member, kind: DeclaredFnMember } + ]) +} diff --git a/src/v2/test/claim/match_binder/match_binder_typing_test.dag b/src/v2/test/claim/match_binder/match_binder_typing_test.dag index bdece9299d3..a1a69ae4b01 100644 --- a/src/v2/test/claim/match_binder/match_binder_typing_test.dag +++ b/src/v2/test/claim/match_binder/match_binder_typing_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.match_binder.match_binder_typing +import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.compiler.resolve { ResolvedTree } import v2.compiler.infer { infer, inferred_facts_resolved_type } import v2.std.qualified_name { declaration_reference_path_optional, lexical_reference_label_optional, qualified_name_last_segment } @@ -731,7 +732,8 @@ fn mbt_resolved() -> ResolvedTree { symbol_index: mbt_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), - unavailable_providers: [] + unavailable_providers: [], + member_kinds: no_member_declaration_kinds() } } diff --git a/src/v2/test/claim/reference_evidence/declaration_reference_evidence_test.dag b/src/v2/test/claim/reference_evidence/declaration_reference_evidence_test.dag index 3841a9065f5..fd5463354f6 100644 --- a/src/v2/test/claim/reference_evidence/declaration_reference_evidence_test.dag +++ b/src/v2/test/claim/reference_evidence/declaration_reference_evidence_test.dag @@ -1,5 +1,6 @@ module v2.test.claim.reference_evidence.declaration_reference_evidence +import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.compiler.resolve { ResolvedTree } import v2.std.symbol_index { symbol_index_lookup } import v2.compiler.infer { infer, inferred_facts_grounding_derived, infer_type_equal_ignoring_provenance } @@ -333,7 +334,8 @@ fn dre_same_leaf_resolved() -> ResolvedTree { symbol_index: call.symbol_index, resolved_declarations: symbol_index_insert(index: call.resolved_declarations, qualified_path: [^p, ^Wrap], resolved: dre_same_leaf_wrap_declaration()), lexical_bindings: call.lexical_bindings, - unavailable_providers: call.unavailable_providers + unavailable_providers: call.unavailable_providers, + member_kinds: no_member_declaration_kinds() } } diff --git a/src/v2/test/lens_common/infer_fixture.dag b/src/v2/test/lens_common/infer_fixture.dag index c6d2cca2bd4..a77e6441a48 100644 --- a/src/v2/test/lens_common/infer_fixture.dag +++ b/src/v2/test/lens_common/infer_fixture.dag @@ -1,4 +1,5 @@ module v2.test.lens_common.infer_fixture +import v2.std.member_declaration_kind { no_member_declaration_kinds } import std.optional { optional_absent } import std.occurrence_identity { OccurrenceSynthetic } @@ -33,7 +34,7 @@ import std.algebra { Cons } // resolution consulted; a supplied tree was never resolved, so it carries an index holding NO // declarations -- the name says so, and a declaration lookup through it finds nothing and refuses. fn claim_resolved_tree_without_declarations(root: Node) -> ResolvedTree { - ResolvedTree { root: root, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] } + ResolvedTree { root: root, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() } } fn claim_atom_node(s: Symbol) -> Node { @@ -234,7 +235,8 @@ fn claim_resolved_call_tree( params: params ), lexical_bindings: empty_map(), - unavailable_providers: [] + unavailable_providers: [], + member_kinds: no_member_declaration_kinds() } } @@ -297,7 +299,8 @@ fn claim_resolved_projection_tree( params: [param] ), lexical_bindings: empty_map(), - unavailable_providers: unavailable + unavailable_providers: unavailable, + member_kinds: no_member_declaration_kinds() } } diff --git a/src/v2/workflow/realization_attempt.dag b/src/v2/workflow/realization_attempt.dag index b0c0be62455..9ce04080435 100644 --- a/src/v2/workflow/realization_attempt.dag +++ b/src/v2/workflow/realization_attempt.dag @@ -1,5 +1,6 @@ module v2.workflow.realization_attempt +import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.compiler.ingested_fixture_arrows { ingested_resolved_module_from_source } import v2.compiler.program_assembly { assemble_program_from_ingest } import v2.compiler.resolve { ResolvedTree } @@ -287,7 +288,7 @@ fn attempt_joined(program: ResolvedTree, fn_name: Symbol, entry: String) -> Entr match list_at_optional(xs: joined, index: 0) { Absent => attempt_refused(entry: entry, phase: PhaseResolve, cause: ^realization_attempt_identity_absent) Present { value: decl } => - match infer_and_discharge(tree: ResolvedTree { root: decl, symbol_index: program.symbol_index, resolved_declarations: program.resolved_declarations, lexical_bindings: program.lexical_bindings, unavailable_providers: program.unavailable_providers }) { + match infer_and_discharge(tree: ResolvedTree { root: decl, symbol_index: program.symbol_index, resolved_declarations: program.resolved_declarations, lexical_bindings: program.lexical_bindings, unavailable_providers: program.unavailable_providers, member_kinds: no_member_declaration_kinds() }) { Rejected { diagnostics: ds } => attempt_refused_at(entry: entry, phase: PhaseInfer, cause: first_located_cause(ds: ds), located: first_located_file(ds: ds)) Accepted { value: inferred, diagnostics: _ } =>