From eddc6e473b38aeb00bed1d9251ef15f894be4f23 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 21:21:18 +0000 Subject: [PATCH 01/10] mandatory_tag gate: read the lowered data-declaration carrier (named nullary Arrow) at normalized/inferred grain Co-Authored-By: Claude Sonnet 5.5 --- src/v2/lens/mandatory_tag.dag | 102 ++++++++++++++++-- .../long/mandatory_tag_gate_witness_test.dag | 34 +++++- 2 files changed, 122 insertions(+), 14 deletions(-) diff --git a/src/v2/lens/mandatory_tag.dag b/src/v2/lens/mandatory_tag.dag index 39a71909c61..220db013d17 100644 --- a/src/v2/lens/mandatory_tag.dag +++ b/src/v2/lens/mandatory_tag.dag @@ -25,7 +25,22 @@ import v2.std.diagnostic { node_locus, outcome_accepted } -import v2.std.node { Atom, Edge, Node, NodeFold, Symbol, TypeNode, fold_node } +import v2.std.node { + Arrow, + ArrowBodyEdge, + Atom, + Authored, + ComputationNode, + StructuralLabel, + Edge, + Node, + NodeFold, + Positional, + Symbol, + TypeNode, + core_edge_label, + fold_node +} import v2.std.node_query { find_named_child } import v2.std.qualified_name { QualifiedName, qualified_name_to_dotted_string } import v2.std.text { String } @@ -75,13 +90,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 +298,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. +fn mandatory_tag_is_arrow(n: Node) -> Bool { + match n.kind { + TypeNode { connective: Arrow } => true + TypeNode { connective: _ } => false + ComputationNode { behavior: _ } => false + } +} + +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 } + }) +} + +fn mandatory_tag_lowered_member(n: Node, required_name: Symbol) -> Optional { + fold(n.children, init: optional_absent(), f: fn(acc, e) { + match e.label { + Authored { name: nm } => + if (nm == required_name) && mandatory_tag_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 mandatory_tag_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 mandatory_tag_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 { @@ -318,6 +397,10 @@ fn mandatory_tag_scan_decls(subtree: Node, required_name: Symbol) -> MandatoryTa MandatoryTagDeclScan { found: optional_absent(), projection_gated_count: 1 } } } else { + match mandatory_tag_lowered_member(n: subtree, required_name: required_name) { + Present { value: arrow } => + MandatoryTagDeclScan { found: optional_present(value: arrow), projection_gated_count: 0 } + Absent => fold(subtree.children, init: MandatoryTagDeclScan { found: optional_absent(), projection_gated_count: 0 }, f: fn(acc, e) { match acc.found { Present { value: _ } => acc @@ -329,6 +412,7 @@ fn mandatory_tag_scan_decls(subtree: Node, required_name: Symbol) -> MandatoryTa } } }) + } } } @@ -407,7 +491,7 @@ fn mandatory_tag_value_findings(d: Node, region: MandatoryTagRegion) -> List - if mandatory_tag_subtree_has_production(n: v, want: ^dag_surface_expr) { + if mandatory_tag_is_arrow(n: d) || mandatory_tag_subtree_has_production(n: v, want: ^dag_surface_expr) { [mandatory_tag_value_unreadable_diagnostic(d: d)] } else { [] 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 fced0a34d56..2b21323be51 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 @@ -27,12 +27,15 @@ 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 every arm the parse grain does except +// the misnamed-anchor spelling variants. 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. @@ -75,7 +78,7 @@ 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 } + Accepted { value: normalized, diagnostics: _ } => GrainTree { root: normalized.root } } } } @@ -172,6 +175,27 @@ test fn mandatory_tag_normalized_grain_misnamed_rejects() -> Bool { ) } +test fn mandatory_tag_normalized_grain_wrong_type_rejects() -> Bool { + gate_rejects_tree_with( + probe: normalized_grain_tree(source: src_wrong_type), + reason: ^mandatory_tag_required_decl_type_mismatch + ) +} + +test fn mandatory_tag_normalized_grain_file_scheme_rejects() -> Bool { + gate_rejects_tree_with( + probe: normalized_grain_tree(source: src_file_scheme), + reason: ^mandatory_tag_value_not_accepted + ) +} + +test fn mandatory_tag_normalized_grain_bogus_scheme_rejects() -> Bool { + gate_rejects_tree_with( + probe: normalized_grain_tree(source: src_bogus_scheme), + reason: ^mandatory_tag_value_vocabulary_unreadable + ) +} + fn roster_rejects_with(probe: GrainProbe, reason: Symbol) -> Bool { match probe { GrainStageRejected => false From 1b8f2d1ab381b78a35bea82810ac48dd3856036a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 22:57:28 +0000 Subject: [PATCH 02/10] mandatory_tag witness: drop three new normalized-grain reds that exceed the new-witness eval-step budget Co-Authored-By: Claude Sonnet 5.5 --- .../long/mandatory_tag_gate_witness_test.dag | 26 +++---------------- 1 file changed, 3 insertions(+), 23 deletions(-) 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 2b21323be51..515198b6779 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 @@ -32,8 +32,9 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // vocabulary), so every arm is exercised there, including the misnamed-anchor control - the exact // #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 every arm the parse grain does except -// the misnamed-anchor spelling variants. Regression receipt: the 2026-07-22 12/12 run predates that +// 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 @@ -175,27 +176,6 @@ test fn mandatory_tag_normalized_grain_misnamed_rejects() -> Bool { ) } -test fn mandatory_tag_normalized_grain_wrong_type_rejects() -> Bool { - gate_rejects_tree_with( - probe: normalized_grain_tree(source: src_wrong_type), - reason: ^mandatory_tag_required_decl_type_mismatch - ) -} - -test fn mandatory_tag_normalized_grain_file_scheme_rejects() -> Bool { - gate_rejects_tree_with( - probe: normalized_grain_tree(source: src_file_scheme), - reason: ^mandatory_tag_value_not_accepted - ) -} - -test fn mandatory_tag_normalized_grain_bogus_scheme_rejects() -> Bool { - gate_rejects_tree_with( - probe: normalized_grain_tree(source: src_bogus_scheme), - reason: ^mandatory_tag_value_vocabulary_unreadable - ) -} - fn roster_rejects_with(probe: GrainProbe, reason: Symbol) -> Bool { match probe { GrainStageRejected => false From 19e84431d7dd469a857fad969a5decb067b94731 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 03:21:15 +0000 Subject: [PATCH 03/10] mandatory_tag: classify the lowered data decl by carried member-kind provenance (normalize -> ResolvedTree -> gate) A lowered data decl and a zero-arg fn are one shape; the authored kind is captured from the parse in normalize, carried on ResolvedTree.member_kinds keyed by declaring module+name, and mandatory_tag refuses when provenance is unavailable. Supplied-carrier controls added. Co-Authored-By: Claude Sonnet 5.5 --- src/v2/compiler/00_compile.dag | 43 +++- src/v2/compiler/03_ingest.dag | 5 +- src/v2/compiler/03_name_resolve.dag | 29 ++- src/v2/compiler/03_normalize.dag | 61 ++++- src/v2/compiler/03_resolve.dag | 71 +++++- src/v2/compiler/normalized_tree.dag | 29 ++- .../compiler/self_host/closure_emission.dag | 3 +- src/v2/lens/mandatory_tag.dag | 126 +++++++++-- src/v2/std/member_declaration_kind.dag | 95 ++++++++ .../arrow_order_edge/admission_wall_test.dag | 3 +- .../infer_fold_member_instance_test.dag | 3 +- ...nstruct_field_inhabitance_witness_test.dag | 2 +- .../kernel_value_type_roster_witness_test.dag | 2 +- ...lassical_not_ingested_equals_eval_test.dag | 3 +- .../long/mandatory_tag_gate_witness_test.dag | 212 +++++++++++++++++- .../match_binder/match_binder_typing_test.dag | 4 +- .../declaration_reference_evidence_test.dag | 4 +- src/v2/test/lens_common/infer_fixture.dag | 9 +- src/v2/workflow/realization_attempt.dag | 3 +- 19 files changed, 639 insertions(+), 68 deletions(-) create mode 100644 src/v2/std/member_declaration_kind.dag diff --git a/src/v2/compiler/00_compile.dag b/src/v2/compiler/00_compile.dag index c39846fb6cd..aee4b4925f2 100644 --- a/src/v2/compiler/00_compile.dag +++ b/src/v2/compiler/00_compile.dag @@ -44,6 +44,7 @@ import gunbc.instruments.type_declaration_use_census { TypeCensusContribution, AsTypedBy, AsUntyped, type_census_contribution, type_census_unreached } import v2.compiler.name_resolve { + subject_member_kind_channel, resolution_context_namespace, closure_declarations_demand, Admission, @@ -200,7 +201,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 +797,34 @@ fn machine_shape_root_gate(tree: InferredTree) -> Outcome> { machine_shape_compile_gate(node: tree.root) } +// The native door's channel for its resolved subject, read from the same validated roots resolve_in_context reads. +// A duplicate-member refusal cannot be returned from this verdict, so it reads as Unavailable and mandatory_tag +// refuses on provenance -- never "fine", never "every module lacks its data decl". +fn native_subject_member_kinds(shared: ResolutionContext, resolved: Node) -> MemberKindChannel { + match qualified_name_from_module_node(root: resolved) { + Rejected { diagnostics: _ } => no_member_declaration_kinds() + Accepted { value: qn, diagnostics: _ } => + match subject_member_kind_channel(roots: shared.roots, name: qn) { + Accepted { value: c, diagnostics: _ } => c + Rejected { diagnostics: _ } => no_member_declaration_kinds() + } + } +} + +// 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 +1072,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 +3540,7 @@ fn native_module_resolve_verdict( symbol_index: shared.symbol_index, closure_declarations: closure.declarations, unavailable_providers: closure.refused, + member_kinds: native_subject_member_kinds(shared: shared, resolved: resolved), 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 220db013d17..22a736272af 100644 --- a/src/v2/lens/mandatory_tag.dag +++ b/src/v2/lens/mandatory_tag.dag @@ -44,6 +44,17 @@ import v2.std.node { 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 { @@ -340,19 +351,27 @@ fn mandatory_tag_lowered_body(d: Node) -> Optional { }) } -fn mandatory_tag_lowered_member(n: Node, required_name: Symbol) -> Optional { - fold(n.children, init: optional_absent(), f: fn(acc, e) { - match e.label { - Authored { name: nm } => - if (nm == required_name) && mandatory_tag_is_arrow(n: e.target) { - 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) && mandatory_tag_is_arrow(n: e.target) { + optional_present(value: e.target) + } else { + acc + } + StructuralLabel { label: _ } => acc + Positional => acc } - StructuralLabel { label: _ } => acc - Positional => acc - } - }) + }) + } } fn mandatory_tag_decl_type_node(d: Node) -> Optional { @@ -397,10 +416,6 @@ fn mandatory_tag_scan_decls(subtree: Node, required_name: Symbol) -> MandatoryTa MandatoryTagDeclScan { found: optional_absent(), projection_gated_count: 1 } } } else { - match mandatory_tag_lowered_member(n: subtree, required_name: required_name) { - Present { value: arrow } => - MandatoryTagDeclScan { found: optional_present(value: arrow), projection_gated_count: 0 } - Absent => fold(subtree.children, init: MandatoryTagDeclScan { found: optional_absent(), projection_gated_count: 0 }, f: fn(acc, e) { match acc.found { Present { value: _ } => acc @@ -412,7 +427,6 @@ fn mandatory_tag_scan_decls(subtree: Node, required_name: Symbol) -> MandatoryTa } } }) - } } } @@ -424,6 +438,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, @@ -510,10 +532,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( @@ -528,7 +585,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)] } @@ -538,7 +605,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: _ } => [] @@ -550,7 +617,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 ) ) }) @@ -565,22 +633,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..72b0d8c00cf --- /dev/null +++ b/src/v2/std/member_declaration_kind.dag @@ -0,0 +1,95 @@ +module v2.std.member_declaration_kind + +import std.types { List } +import std.algebra { Empty, FreeMonoid, list_snoc_item } +import v2.std.algebra { fold_list, length } +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. +fn declared_members_have_duplicate(members: FreeMonoid) -> Bool { + fold_list( + xs: members, + empty: false, + cons: fn(acc, m) { + acc || (length(xs: fold_list(xs: members, empty: Empty, cons: fn(hits, o) { if o.name == m.name { list_snoc_item(xs: hits, item: o) } else { hits } })) > 1) + } + ) +} 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 cdf1a02a6f4..feb8d9bbed0 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 } @@ -80,7 +81,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 515198b6779..adeb36c3d1e 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,22 @@ 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 { + 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, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } +import v2.lens.mandatory_tag { mandatory_tag_lowered_candidate_findings, extdeps_external_authority_region } import std.algebra { Cons, Empty } import v2.std.collection { empty_map} import v2.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } @@ -59,7 +74,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() @@ -68,7 +83,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() } } } } @@ -79,7 +94,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 } + } } } } @@ -87,8 +106,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 } @@ -98,8 +117,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 { @@ -179,7 +198,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 @@ -202,3 +221,178 @@ test fn mandatory_tag_enrolled_in_root_roster_rejects_violating_module() -> Bool reason: ^mandatory_tag_missing_required_decl ) } + + +// 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 -- normalize capturing the kinds, resolve carrying them, the door binding them to the gate -- is +// run for real by mandatory_tag_normalized_grain_clean_accepts above; deleting that integration makes it fail. +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 + } +} + +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: _ } => From fdfbb71875f1a915b5214a32acd7e6634d9b12d7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 04:12:09 +0000 Subject: [PATCH 04/10] member-kind channel: one-pass duplicate check (map, not rescan); drop dangling native_subject_member_kinds (no consumer yet) Co-Authored-By: Claude Sonnet 5.5 --- src/v2/compiler/00_compile.dag | 17 +---------------- src/v2/std/member_declaration_kind.dag | 22 ++++++++++++++++------ 2 files changed, 17 insertions(+), 22 deletions(-) diff --git a/src/v2/compiler/00_compile.dag b/src/v2/compiler/00_compile.dag index aee4b4925f2..b84fb9f7a5e 100644 --- a/src/v2/compiler/00_compile.dag +++ b/src/v2/compiler/00_compile.dag @@ -44,7 +44,6 @@ import gunbc.instruments.type_declaration_use_census { TypeCensusContribution, AsTypedBy, AsUntyped, type_census_contribution, type_census_unreached } import v2.compiler.name_resolve { - subject_member_kind_channel, resolution_context_namespace, closure_declarations_demand, Admission, @@ -797,20 +796,6 @@ fn machine_shape_root_gate(tree: InferredTree) -> Outcome> { machine_shape_compile_gate(node: tree.root) } -// The native door's channel for its resolved subject, read from the same validated roots resolve_in_context reads. -// A duplicate-member refusal cannot be returned from this verdict, so it reads as Unavailable and mandatory_tag -// refuses on provenance -- never "fine", never "every module lacks its data decl". -fn native_subject_member_kinds(shared: ResolutionContext, resolved: Node) -> MemberKindChannel { - match qualified_name_from_module_node(root: resolved) { - Rejected { diagnostics: _ } => no_member_declaration_kinds() - Accepted { value: qn, diagnostics: _ } => - match subject_member_kind_channel(roots: shared.roots, name: qn) { - Accepted { value: c, diagnostics: _ } => c - Rejected { diagnostics: _ } => no_member_declaration_kinds() - } - } -} - // 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 { @@ -3540,7 +3525,7 @@ fn native_module_resolve_verdict( symbol_index: shared.symbol_index, closure_declarations: closure.declarations, unavailable_providers: closure.refused, - member_kinds: native_subject_member_kinds(shared: shared, resolved: resolved), + member_kinds: no_member_declaration_kinds(), lexical: lexical ) }, diff --git a/src/v2/std/member_declaration_kind.dag b/src/v2/std/member_declaration_kind.dag index 72b0d8c00cf..cd332a3a74b 100644 --- a/src/v2/std/member_declaration_kind.dag +++ b/src/v2/std/member_declaration_kind.dag @@ -1,8 +1,9 @@ module v2.std.member_declaration_kind import std.types { List } -import std.algebra { Empty, FreeMonoid, list_snoc_item } -import v2.std.algebra { fold_list, length } +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 } @@ -83,13 +84,22 @@ fn member_kind_lookup(channel: MemberKindChannel, module: String, name: Symbol) } // 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 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: false, + empty: MemberNamesSeen { seen: empty_map(), duplicate: false }, cons: fn(acc, m) { - acc || (length(xs: fold_list(xs: members, empty: Empty, cons: fn(hits, o) { if o.name == m.name { list_snoc_item(xs: hits, item: o) } else { hits } })) > 1) + 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 } From 846d16f6f59d85d1c55bfcbae40488c3c3976736 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 04:13:52 +0000 Subject: [PATCH 05/10] rung drop: member-kind door binding (resolve_in_context -> ResolvedTree.member_kinds -> mandatory_tag door lens) executed by no claim Co-Authored-By: Claude Sonnet 5.5 --- ...kind_door_binding_executed_by_no_claim.dag | 37 +++++++++++++++++++ docs/design-rung-drops.md | 4 ++ 2 files changed, 41 insertions(+) create mode 100644 dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag diff --git a/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag b/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag new file mode 100644 index 00000000000..a4a0e2bcf4f --- /dev/null +++ b/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag @@ -0,0 +1,37 @@ +module gunbc.rung_drop.member_kind_door_binding_executed_by_no_claim + +import std.types { List, NonEmptyStr, String } +import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged } +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } + +// DECLARED 2026-10-07 (gunbc#13513, ruling via bold-bee-114). THE DROPPED LINK IS NEW CODE THAT HAS NEVER EXECUTED; this is +// not a rung that stood and was lowered. #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 normalize -> +// member_kind_channel_of_tree -> gate legs execute in test.long.mandatory_tag_gate_witness (real-route clean control, +// zero-arg-fn impersonation, uncovered-module and unread refusals, duplicate detection). 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 +// but executed by no claim: a door-grain control built 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. Measured before it was removed, each door-grain witness cost roughly +// 470-560k eval steps against the 72300 new-witness budget, so once runnable it is a long-lane witness. + +data member_kind_door_binding_executed_by_no_claim_population: List = [ + "v2.compiler.name_resolve resolve_in_context -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance: the door-grain link carrying member-kind provenance to the mandatory_tag root lens, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission", +] + +data member_kind_door_binding_executed_by_no_claim: RungDrop = RungDrop { + identity: "member_kind_door_binding_executed_by_no_claim" as NonEmptyStr, + subject: "door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim", + declared: "2026-10-07", + standing: Standing, + declaration: TypedDeclaration { + previous: MechanicallyPreventable, + temporary: Mitigatable, + reason: ReplacementStaged { + replacement: "a minimal extdeps.* subject accepted through compile_source_root_ingest_with_admission past every roster lens (the member_not_a_binder door refusal, filed as its own item), which makes the door-grain controls runnable" + }, + population: member_kind_door_binding_executed_by_no_claim_population, + restoration_trigger: "THE 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. WHAT THAT MUST BE 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/docs/design-rung-drops.md b/docs/design-rung-drops.md index 92053f93853..8f7bb7b3677 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -268,6 +268,10 @@ Producer: `tools.emission_entry_instrument::measure_entry_emission` production MegaRAC operation admission (gunbc.megarac_managed_host admit_megarac_host) grounds media attach, KVM still and SDR socket naming at the build a managed host's access observation read, which for mtcollins1 is BMC 0.32 (2026-09-05) although the controller was reflashed to 0.45.3 on 2026-10-02; the current-build gate (admit_megarac_host_at_current_build) that refuses this is built and enrolled in shadow: RUNG DROP, structurally guaranteed -> mitigatable (replacement staged: gunbc.megarac_managed_host admit_megarac_host_at_current_build over gunbc.megarac_operation_standing (current build from committed build readings and recorded firmware transitions; operations grounded at an observed baseboard and firmware by receipts joined to a reading of that build with no transition between), rows in gunbc.machine_intake_megarac_operation_evidence). Population: mtcollins1's MegaRAC virtual media attach, KVM canvas still and SDR socket naming as admitted by admit_megarac_host, and the gunbc.machine_intake_mtcollins1_boot_run boot that depends on them -- the only managed host is mtcollins1. Restored when: THE CAPABILITY: EACH OF mtcollins1's MEGARAC OPERATIONS ADMITTED THROUGH THE CURRENT-BUILD GATE FROM A COMMITTED CURRENT-BUILD OBSERVATION PLUS EXECUTED EVIDENCE AT THAT BUILD -- a committed read-only probe of the controller's build (mc info / hpm check) entered as a build reading in gunbc.machine_intake_megarac_operation_evidence, and, for each of media attach, KVM still and SDR socket naming, a committed receipt that joins to that reading with no firmware transition recorded between. SUFFICIENT FOR: switching every production caller from admit_megarac_host to admit_megarac_host_at_current_build in one transition with the boot still admitted. A probe alone, or receipts without a build reading, or a gate that admits some operations while the boot needs all three, does not retire this row. +### door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim — declared 2026-10-07 + +door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: a minimal extdeps.* subject accepted through compile_source_root_ingest_with_admission past every roster lens (the member_not_a_binder door refusal, filed as its own item), which makes the door-grain controls runnable). Population: v2.compiler.name_resolve resolve_in_context -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance: the door-grain link carrying member-kind provenance to the mandatory_tag root lens, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission. Restored when: THE 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. WHAT THAT MUST BE 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. + ### the fleet-uniform slot row (gunbc.runner_slot_desired gunbc_runner_slot_desired): every committed slot on a host carries the same MemoryMax, so width and slice cap are one quotient — declared 2026-09-21 the fleet-uniform slot row (gunbc.runner_slot_desired gunbc_runner_slot_desired): every committed slot on a host carries the same MemoryMax, so width and slice cap are one quotient: RUNG DROP, structurally guaranteed -> mechanically preventable (replacement staged: gunbc.runner_slot_allocation gunbc_runner_slot_desired_for (28 GiB MemoryMax, MemoryHigh at the ceiling, MemorySwapMax zero for srv1_microvm_shakedown_slot) and memory_admitted_width_of_envelope charging that slot first on srv1, checked by test.claim.runner.runner_microvm_slot_controller_witness_test). Population: gunbc.runner_slot_allocation srv1_microvm_shakedown_slot (srv1-13): 30064771072 bytes against the fleet row's 27917287424. Restored when: EITHER the shakedown slot leaves fabric_execution_slot_identities with its cell retired through the modeled teardown, OR the fleet row moves to the shakedown ceiling under an operator ruling cited on that change, so gunbc_runner_slot_desired_for has no differing arm and is deleted. A second per-slot arm satisfies neither. From 159dc8834c3106e1fcf605f1b2e1cab48304e899 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 04:18:20 +0000 Subject: [PATCH 06/10] door-grain gap: record as a GuaranteeStall (new never-executed link, no rung lowered); remove the rung_drop row and its hand-appended doc section Co-Authored-By: Claude Sonnet 5.5 --- ...oor_binding_executed_by_no_claim_stall.dag | 25 +++++++++++++ dag/gunbc/guarantee_stall/roster.dag | 2 + ...kind_door_binding_executed_by_no_claim.dag | 37 ------------------- docs/design-rung-drops.md | 4 -- 4 files changed, 27 insertions(+), 41 deletions(-) create mode 100644 dag/gunbc/guarantee_stall/member_kind_door_binding_executed_by_no_claim_stall.dag delete mode 100644 dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag 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 45f1ec36561..618bcf7254f 100644 --- a/dag/gunbc/guarantee_stall/roster.dag +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -75,6 +75,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 } // THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are // carried here verbatim rather than split across the row modules they describe. Their membership @@ -245,6 +246,7 @@ data all_guarantee_stalls: List = [ compile_pool_provision_wired_but_unreachable_stall, accumulator_copy_untyped_combiner_refusals_stall, keyed_apply_patch_rebuilds_rows_per_hunk_stall, + member_kind_door_binding_executed_by_no_claim_stall, ] // THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES. diff --git a/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag b/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag deleted file mode 100644 index a4a0e2bcf4f..00000000000 --- a/dag/gunbc/rung_drop/member_kind_door_binding_executed_by_no_claim.dag +++ /dev/null @@ -1,37 +0,0 @@ -module gunbc.rung_drop.member_kind_door_binding_executed_by_no_claim - -import std.types { List, NonEmptyStr, String } -import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged } -import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } - -// DECLARED 2026-10-07 (gunbc#13513, ruling via bold-bee-114). THE DROPPED LINK IS NEW CODE THAT HAS NEVER EXECUTED; this is -// not a rung that stood and was lowered. #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 normalize -> -// member_kind_channel_of_tree -> gate legs execute in test.long.mandatory_tag_gate_witness (real-route clean control, -// zero-arg-fn impersonation, uncovered-module and unread refusals, duplicate detection). 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 -// but executed by no claim: a door-grain control built 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. Measured before it was removed, each door-grain witness cost roughly -// 470-560k eval steps against the 72300 new-witness budget, so once runnable it is a long-lane witness. - -data member_kind_door_binding_executed_by_no_claim_population: List = [ - "v2.compiler.name_resolve resolve_in_context -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance: the door-grain link carrying member-kind provenance to the mandatory_tag root lens, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission", -] - -data member_kind_door_binding_executed_by_no_claim: RungDrop = RungDrop { - identity: "member_kind_door_binding_executed_by_no_claim" as NonEmptyStr, - subject: "door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim", - declared: "2026-10-07", - standing: Standing, - declaration: TypedDeclaration { - previous: MechanicallyPreventable, - temporary: Mitigatable, - reason: ReplacementStaged { - replacement: "a minimal extdeps.* subject accepted through compile_source_root_ingest_with_admission past every roster lens (the member_not_a_binder door refusal, filed as its own item), which makes the door-grain controls runnable" - }, - population: member_kind_door_binding_executed_by_no_claim_population, - restoration_trigger: "THE 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. WHAT THAT MUST BE 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/docs/design-rung-drops.md b/docs/design-rung-drops.md index 8f7bb7b3677..92053f93853 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -268,10 +268,6 @@ Producer: `tools.emission_entry_instrument::measure_entry_emission` production MegaRAC operation admission (gunbc.megarac_managed_host admit_megarac_host) grounds media attach, KVM still and SDR socket naming at the build a managed host's access observation read, which for mtcollins1 is BMC 0.32 (2026-09-05) although the controller was reflashed to 0.45.3 on 2026-10-02; the current-build gate (admit_megarac_host_at_current_build) that refuses this is built and enrolled in shadow: RUNG DROP, structurally guaranteed -> mitigatable (replacement staged: gunbc.megarac_managed_host admit_megarac_host_at_current_build over gunbc.megarac_operation_standing (current build from committed build readings and recorded firmware transitions; operations grounded at an observed baseboard and firmware by receipts joined to a reading of that build with no transition between), rows in gunbc.machine_intake_megarac_operation_evidence). Population: mtcollins1's MegaRAC virtual media attach, KVM canvas still and SDR socket naming as admitted by admit_megarac_host, and the gunbc.machine_intake_mtcollins1_boot_run boot that depends on them -- the only managed host is mtcollins1. Restored when: THE CAPABILITY: EACH OF mtcollins1's MEGARAC OPERATIONS ADMITTED THROUGH THE CURRENT-BUILD GATE FROM A COMMITTED CURRENT-BUILD OBSERVATION PLUS EXECUTED EVIDENCE AT THAT BUILD -- a committed read-only probe of the controller's build (mc info / hpm check) entered as a build reading in gunbc.machine_intake_megarac_operation_evidence, and, for each of media attach, KVM still and SDR socket naming, a committed receipt that joins to that reading with no firmware transition recorded between. SUFFICIENT FOR: switching every production caller from admit_megarac_host to admit_megarac_host_at_current_build in one transition with the boot still admitted. A probe alone, or receipts without a build reading, or a gate that admits some operations while the boot needs all three, does not retire this row. -### door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim — declared 2026-10-07 - -door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> door-binding link is compiled but executed by no claim: RUNG DROP, mechanically preventable -> mitigatable (replacement staged: a minimal extdeps.* subject accepted through compile_source_root_ingest_with_admission past every roster lens (the member_not_a_binder door refusal, filed as its own item), which makes the door-grain controls runnable). Population: v2.compiler.name_resolve resolve_in_context -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance: the door-grain link carrying member-kind provenance to the mandatory_tag root lens, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission. Restored when: THE 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. WHAT THAT MUST BE 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. - ### the fleet-uniform slot row (gunbc.runner_slot_desired gunbc_runner_slot_desired): every committed slot on a host carries the same MemoryMax, so width and slice cap are one quotient — declared 2026-09-21 the fleet-uniform slot row (gunbc.runner_slot_desired gunbc_runner_slot_desired): every committed slot on a host carries the same MemoryMax, so width and slice cap are one quotient: RUNG DROP, structurally guaranteed -> mechanically preventable (replacement staged: gunbc.runner_slot_allocation gunbc_runner_slot_desired_for (28 GiB MemoryMax, MemoryHigh at the ceiling, MemorySwapMax zero for srv1_microvm_shakedown_slot) and memory_admitted_width_of_envelope charging that slot first on srv1, checked by test.claim.runner.runner_microvm_slot_controller_witness_test). Population: gunbc.runner_slot_allocation srv1_microvm_shakedown_slot (srv1-13): 30064771072 bytes against the fleet row's 27917287424. Restored when: EITHER the shakedown slot leaves fabric_execution_slot_identities with its cell retired through the modeled teardown, OR the fleet row moves to the shakedown ceiling under an operator ruling cited on that change, so gunbc_runner_slot_desired_for has no differing arm and is deleted. A second per-slot arm satisfies neither. From 9622d1eefa003cd713eceea90210c0d4286db7f7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 14:55:59 +0000 Subject: [PATCH 07/10] mandatory_tag witness: top-level selector control (nested anchor under unrelated member refuses); annotation states what is executed Co-Authored-By: Claude Sonnet 5.5 --- .../long/mandatory_tag_gate_witness_test.dag | 52 +++++++++++++++++-- 1 file changed, 49 insertions(+), 3 deletions(-) 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 adeb36c3d1e..fd85fd6808b 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 @@ -21,7 +21,7 @@ import v2.std.member_declaration_kind { } import v2.std.qualified_name { QualifiedName } import std.occurrence_identity { OccurrenceSynthetic } -import v2.std.node { Arrow, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } +import v2.std.node { Arrow, Authored, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } import v2.lens.mandatory_tag { mandatory_tag_lowered_candidate_findings, extdeps_external_authority_region } import std.algebra { Cons, Empty } import v2.std.collection { empty_map} @@ -188,6 +188,49 @@ test fn mandatory_tag_normalized_grain_missing_rejects() -> Bool { ) } +// TOP-LEVEL SELECTOR CONTROL. The module's only direct member is UNRELATED; the required name appears only +// NESTED inside that member's Arrow, as a valid Arrow, and the supplied channel would admit that name as a +// data member. The gate must still refuse as missing: restoring a recursive subtree search for the lowered +// member turns this red. Nesting is planted into the REAL normalized tree of src_missing. +fn mt_plant_nested_anchor(n: Node) -> Node { + let kids = fold(n.children, init: [], f: fn(acc, e) { + concat(acc, [Edge { label: e.label, target: mt_plant_nested_anchor(n: e.target) }]) + }) + match n.kind { + TypeNode { connective: Arrow } => + Node { + kind: n.kind, + children: concat(kids, [Edge { + label: Authored { name: ^extdeps_external_authority_anchor }, + target: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]) + }]), + occurrence_id: n.occurrence_id + } + _ => Node { kind: n.kind, children: kids, occurrence_id: n.occurrence_id } + } +} + +test fn mandatory_tag_normalized_grain_nested_anchor_under_unrelated_member_rejects() -> Bool { + match normalized_grain_tree(source: src_missing) { + GrainStageRejected => false + GrainTree { root: root, channel: _ } => + gate_rejects_tree_with( + probe: GrainTree { + root: mt_plant_nested_anchor(n: root), + channel: MemberKindsCaptured { + covered: [[^extdeps, ^gate_probe_missing]], + members: [QualifiedDeclaredMember { + module: [^extdeps, ^gate_probe_missing], + name: ^extdeps_external_authority_anchor, + kind: DeclaredDataMember + }] + } + }, + reason: ^mandatory_tag_missing_required_decl + ) + } +} + test fn mandatory_tag_normalized_grain_misnamed_rejects() -> Bool { gate_rejects_tree_with( probe: normalized_grain_tree(source: src_misnamed), @@ -225,8 +268,11 @@ test fn mandatory_tag_enrolled_in_root_roster_rejects_violating_module() -> Bool // 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 -- normalize capturing the kinds, resolve carrying them, the door binding them to the gate -- is -// run for real by mandatory_tag_normalized_grain_clean_accepts above; deleting that integration makes it fail. +// 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 } } From e8837d9a7a9966df5ca558248631ae9c65af7c42 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 15:10:45 +0000 Subject: [PATCH 08/10] mandatory_tag witness: cheap supplied grafted-module selector control (nested anchor under unrelated member) + direct-anchor positive twin Co-Authored-By: Claude Sonnet 5.5 --- .../long/mandatory_tag_gate_witness_test.dag | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) 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 fd85fd6808b..e628d3d57c9 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 @@ -20,6 +20,7 @@ import v2.std.member_declaration_kind { no_member_declaration_kinds } import v2.std.qualified_name { QualifiedName } +import v2.compiler.namespace_graft { namespace_graft_build_body_conj, namespace_graft_fold_spine, namespace_graft_wrap_module_shell } import std.occurrence_identity { OccurrenceSynthetic } import v2.std.node { Arrow, Authored, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } import v2.lens.mandatory_tag { mandatory_tag_lowered_candidate_findings, extdeps_external_authority_region } @@ -367,6 +368,58 @@ fn mt_only(candidate: Node, channel: MemberKindChannel, reason: Symbol) -> Bool } } +// 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: GrainTree { 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: GrainTree { 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 From 36f294844a902ef2cfa538c322bc87ae4f8a3486 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 15:22:26 +0000 Subject: [PATCH 09/10] mandatory_tag: move cheap supplied-carrier controls to a fast-lane witness module; drop the redundant real-normalize nested control Co-Authored-By: Claude Sonnet 5.5 --- .../long/mandatory_tag_gate_witness_test.dag | 288 +----------------- ...tory_tag_supplied_carrier_witness_test.dag | 285 +++++++++++++++++ 2 files changed, 286 insertions(+), 287 deletions(-) create mode 100644 src/v2/test/claim/mandatory_tag_supplied_carrier_witness_test.dag 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 e628d3d57c9..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 @@ -9,21 +9,8 @@ import v2.compiler.infer { InferredTree } import v2.extdeps.languages.dag { dag_language_model } 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 { - DeclaredDataMember, - DeclaredFnMember, - DeclaredMember, - MemberKindChannel, - MemberKindsCaptured, - QualifiedDeclaredMember, - declared_members_have_duplicate, - no_member_declaration_kinds -} -import v2.std.qualified_name { QualifiedName } +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.occurrence_identity { OccurrenceSynthetic } -import v2.std.node { Arrow, Authored, ArrowBodyEdge, Atom, Edge, Node, Positional, TypeNode, Conj, core_edge_label } -import v2.lens.mandatory_tag { mandatory_tag_lowered_candidate_findings, extdeps_external_authority_region } import std.algebra { Cons, Empty } import v2.std.collection { empty_map} import v2.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } @@ -189,49 +176,6 @@ test fn mandatory_tag_normalized_grain_missing_rejects() -> Bool { ) } -// TOP-LEVEL SELECTOR CONTROL. The module's only direct member is UNRELATED; the required name appears only -// NESTED inside that member's Arrow, as a valid Arrow, and the supplied channel would admit that name as a -// data member. The gate must still refuse as missing: restoring a recursive subtree search for the lowered -// member turns this red. Nesting is planted into the REAL normalized tree of src_missing. -fn mt_plant_nested_anchor(n: Node) -> Node { - let kids = fold(n.children, init: [], f: fn(acc, e) { - concat(acc, [Edge { label: e.label, target: mt_plant_nested_anchor(n: e.target) }]) - }) - match n.kind { - TypeNode { connective: Arrow } => - Node { - kind: n.kind, - children: concat(kids, [Edge { - label: Authored { name: ^extdeps_external_authority_anchor }, - target: mt_candidate(codomain: ^ExternalAuthority, body: [^Https]) - }]), - occurrence_id: n.occurrence_id - } - _ => Node { kind: n.kind, children: kids, occurrence_id: n.occurrence_id } - } -} - -test fn mandatory_tag_normalized_grain_nested_anchor_under_unrelated_member_rejects() -> Bool { - match normalized_grain_tree(source: src_missing) { - GrainStageRejected => false - GrainTree { root: root, channel: _ } => - gate_rejects_tree_with( - probe: GrainTree { - root: mt_plant_nested_anchor(n: root), - channel: MemberKindsCaptured { - covered: [[^extdeps, ^gate_probe_missing]], - members: [QualifiedDeclaredMember { - module: [^extdeps, ^gate_probe_missing], - name: ^extdeps_external_authority_anchor, - kind: DeclaredDataMember - }] - } - }, - reason: ^mandatory_tag_missing_required_decl - ) - } -} - test fn mandatory_tag_normalized_grain_misnamed_rejects() -> Bool { gate_rejects_tree_with( probe: normalized_grain_tree(source: src_misnamed), @@ -265,233 +209,3 @@ test fn mandatory_tag_enrolled_in_root_roster_rejects_violating_module() -> Bool reason: ^mandatory_tag_missing_required_decl ) } - - -// 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: GrainTree { 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: GrainTree { 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/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 } + ]) +} From ca206cd1557f536a4522ee0336f2c5d73168fc92 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 15:43:50 +0000 Subject: [PATCH 10/10] mandatory_tag: use one node_is_arrow accessor in v2.std.node instead of a private copy (review 77607) Co-Authored-By: Claude Sonnet 5.5 --- src/v2/lens/mandatory_tag.dag | 20 ++++++-------------- src/v2/std/node.dag | 10 ++++++++++ 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/src/v2/lens/mandatory_tag.dag b/src/v2/lens/mandatory_tag.dag index 22a736272af..1f798fcae49 100644 --- a/src/v2/lens/mandatory_tag.dag +++ b/src/v2/lens/mandatory_tag.dag @@ -26,7 +26,6 @@ import v2.std.diagnostic { outcome_accepted } import v2.std.node { - Arrow, ArrowBodyEdge, Atom, Authored, @@ -39,7 +38,8 @@ import v2.std.node { Symbol, TypeNode, core_edge_label, - fold_node + fold_node, + node_is_arrow } import v2.std.node_query { find_named_child } import v2.std.qualified_name { QualifiedName, qualified_name_to_dotted_string } @@ -317,14 +317,6 @@ fn mandatory_tag_decl_name(d: Node) -> MandatoryTagDeclName { // 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. -fn mandatory_tag_is_arrow(n: Node) -> Bool { - match n.kind { - TypeNode { connective: Arrow } => true - TypeNode { connective: _ } => false - ComputationNode { behavior: _ } => false - } -} - type MandatoryTagPositionalScan { seen: Int second: Optional @@ -362,7 +354,7 @@ fn mandatory_tag_lowered_member(module_node: Node, required_name: Symbol) -> Opt fold(body.children, init: optional_absent(), f: fn(acc, e) { match e.label { Authored { name: nm } => - if (nm == required_name) && mandatory_tag_is_arrow(n: e.target) { + if (nm == required_name) && node_is_arrow(n: e.target) { optional_present(value: e.target) } else { acc @@ -375,7 +367,7 @@ fn mandatory_tag_lowered_member(module_node: Node, required_name: Symbol) -> Opt } fn mandatory_tag_decl_type_node(d: Node) -> Optional { - if mandatory_tag_is_arrow(n: d) { + 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) { @@ -386,7 +378,7 @@ fn mandatory_tag_decl_type_node(d: Node) -> Optional { } fn mandatory_tag_decl_value_node(d: Node) -> Optional { - if mandatory_tag_is_arrow(n: d) { + 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) { @@ -513,7 +505,7 @@ fn mandatory_tag_value_findings(d: Node, region: MandatoryTagRegion) -> List - if mandatory_tag_is_arrow(n: d) || 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 { [] 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,