Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
7a65ca7
Stop record-field lenses from refusing module containers as binders.
Oct 8, 2026
1dc5e32
Merge origin/main into session/swift-ant-420
Oct 8, 2026
e04cb5d
Prove the compile door admits a minimal extdeps module past the lens …
Oct 8, 2026
c89af7e
Admit the door-grain probe as an exempt extdeps.fixture module.
Oct 8, 2026
3a31f01
Stop compile-door lenses from judging function and parse payloads as …
Oct 8, 2026
719c026
Judge mixed Conj siblings; skip only module-surface and function memb…
Oct 8, 2026
ed79aa2
Drive the door-grain control through compile_door_ledger import-closu…
Oct 8, 2026
1682e0e
Keep per-edge Conj skips; do not claim-run the hanging ledger import-…
Oct 8, 2026
ffd271d
Skip only module-surface and fn-decl members; restore subtree fold_node.
Oct 8, 2026
23c134f
Restore fact_density NoFact refusal and kernel-ambient identities.
Oct 8, 2026
eaa3b52
Keep member_not_a_binder ownership; restore Arrow-param and identity-…
Oct 8, 2026
f75f3c7
Attach the door-ledger cost note to ledger_style_fatal_or_admitted.
Oct 8, 2026
62ceef3
Dump the lowered fn member the door lenses see.
Oct 8, 2026
ff60ef7
Keep dag_node_is_fn_decl as fn-decl only; skip test-fn at the member-…
Oct 8, 2026
eb021e0
Disposition the identity predicates; skip parse-projection names only…
Oct 8, 2026
1970538
Require door admitted after infer; do not treat find_witness as lens …
Oct 8, 2026
cf0e72a
Demote the red door Bool to a dump; cite #13513 not a missing stall row.
Oct 8, 2026
da66dfb
Drop the unread identity-skip debt rows and the header-edge module-su…
Oct 8, 2026
71c241d
Drop the unread compile-door dump module; stop claiming the door is g…
Oct 8, 2026
ff4a859
Reuse the graft Conj predicate and one module-surface identity set.
Oct 8, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions src/v2/extdeps/languages/dag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -7610,6 +7610,60 @@ fn namespace_graft_node_is_conj(node: Node) -> Bool {
// would re-create the one-Named-Conj level the fill misreads.
data namespace_graft_module_body_identity: Symbol = ^namespace_graft_module_body

fn dag_identity_is_module_surface(id: Symbol) -> Bool {
(id == ^dag_surface_module) || (id == namespace_graft_module_body_identity)
}

// A MODULE SURFACE is identified by what the node IS: parse/emit production identity
// dag_surface_module, the graft body's producer stamp, or a synthetic Atom whose
// identity is dag_surface_module. A header child edge is not identity (review 77909).
fn dag_node_is_module_surface(node: Node) -> Bool {
match parse_production_emitted_identity_optional(node: node) {
Present { value: id } => dag_identity_is_module_surface(id: id)
Absent =>
match node_atom_identity_optional(node: node) {
Present { value: id } => dag_identity_is_module_surface(id: id)
Absent => false
}
}
}

// THE RECORD-FIELD CARRIER PREDICATE the unit-modeling and lifecycle-carrier lenses share.
// A Conj is a record-field carrier unless THIS NODE is a module surface. A sibling that
// happens to be a module surface does not opt the whole Conj out (DESIGN §5: refuse the
// member, never widen to the container). Other connectives are not record payloads; Disj
// arm payloads are Conjs and are judged when those Conjs are visited.
fn dag_node_is_record_field_carrier(node: Node) -> Bool {
namespace_graft_node_is_conj(node: node) && !dag_node_is_module_surface(node: node)
}

fn dag_authored_name_is_parse_production_projection(name: Symbol) -> Bool {
(name == ^grammar_production_identity_node_projection) ||
(name == ^grammar_production_captured_node_projection)
}

// Stamp edges on a MODULE SURFACE only. Same spelling on an ordinary record is a user field
// and must still be judged (DESIGN §5: refuse, never widen).
fn dag_edge_is_module_surface_parse_projection(carrier: Node, name: Symbol) -> Bool {
dag_node_is_module_surface(node: carrier) &&
dag_authored_name_is_parse_production_projection(name: name)
}

// Per-edge skip by identity only (DESIGN §5: refuse, never widen). A non-binder record
// field that is an Atom or Disj must still be member_not_a_binder. fn-decl is the
// production identity dag_surface_fn_decl (unchanged meaning for other callers).
// test-fn identity lives only here, not in dag_node_is_fn_decl.
fn dag_node_is_namespace_member_target(node: Node) -> Bool {
if dag_node_is_module_surface(node: node) || dag_node_is_fn_decl(node: node) {
true
} else {
match parse_production_emitted_identity_optional(node: node) {
Present { value: id } => id == ^dag_surface_test_fn_decl
Absent => false
}
}
}

// The one constructor of the marker node: emitted by namespace_graft_build_body_conj.
// It is a surface identity atom, not a type denotation, so infer grounds it with the
// grammar authority's surface-production type (dag_grammar_production_member_declared_type)
Expand Down
13 changes: 9 additions & 4 deletions src/v2/lens/fact_density.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ module v2.lens.fact_density

import std.nat { Nat, Succ, Zero }
import v2.std.node { Authored, StructuralLabel }
import v2.extdeps.languages.dag { dag_node_is_module_surface }
import v2.lens.common.construction_justification { ConstructionJustification }

import v2.std.witness { Holds }
Expand Down Expand Up @@ -61,10 +62,14 @@ fn connective_spec_fact(c: Connective, named_facts: Nat) -> SourceSpecReadFact {
}

fn carrier_spec_fact(carrier: Node) -> SourceSpecReadFact {
match carrier.kind {
ComputationNode { behavior: _ } => NotATypeCarrier
TypeNode { connective: c } =>
connective_spec_fact(c: c, named_facts: named_fact_count(children: carrier.children))
if dag_node_is_module_surface(node: carrier) {
NotATypeCarrier
} else {
match carrier.kind {
ComputationNode { behavior: _ } => NotATypeCarrier
TypeNode { connective: c } =>
connective_spec_fact(c: c, named_facts: named_fact_count(children: carrier.children))
}
}
}
// Node-local predicate (DESIGN 6 bare-minimum-cost): carrier_spec_fact reads only the node's direct
Expand Down
44 changes: 28 additions & 16 deletions src/v2/lens/lifecycle_carrier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,17 +14,20 @@ import v2.std.diagnostic {
}
import v2.std.witness { Holds, Witness }
import v2.std.node {
ComputationNode,
Edge,
Authored,
Node,
Positional,
Symbol,
TypeNode,
symbol_lexeme,
StructuralLabel,
}
import v2.std.node_query { edge_field_type_name, member_edge_type_node, member_not_a_binder_diagnostic }
import v2.extdeps.languages.dag {
dag_edge_is_module_surface_parse_projection,
dag_node_is_namespace_member_target,
dag_node_is_record_field_carrier
}
import std.optional {
Absent,
Optional,
Expand Down Expand Up @@ -115,27 +118,36 @@ fn lifecycle_carrier_diagnostic(carrier: Node) -> Diagnostic {
fn field_lifecycle_violation(carrier: Node, edge: Edge) -> Optional<Diagnostic> {
match edge.label {
Authored { name: nm } =>
match member_edge_type_node(e: edge) {
Absent => optional_present(value: member_not_a_binder_diagnostic(e: edge))
Present { value: t } =>
if type_is_bare_string(target: t) && name_is_lifecycle_field(name: nm) {
optional_present(value: lifecycle_carrier_diagnostic(carrier: carrier))
} else {
optional_absent()
}
if dag_edge_is_module_surface_parse_projection(carrier: carrier, name: nm) {
optional_absent()
} else {
match member_edge_type_node(e: edge) {
Absent =>
if dag_node_is_namespace_member_target(node: edge.target) {
optional_absent()
} else {
optional_present(value: member_not_a_binder_diagnostic(e: edge))
}
Present { value: t } =>
if type_is_bare_string(target: t) && name_is_lifecycle_field(name: nm) {
optional_present(value: lifecycle_carrier_diagnostic(carrier: carrier))
} else {
optional_absent()
}
}
}
StructuralLabel { label: _ } => optional_absent()
Positional => optional_absent()
}
}

fn carrier_first_lifecycle_violation(carrier: Node) -> Optional<Diagnostic> {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_lifecycle_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
if dag_node_is_record_field_carrier(node: carrier) {
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_lifecycle_violation(carrier: carrier, edge: edge))
})
} else {
optional_absent()
}
}

Expand Down
5 changes: 5 additions & 0 deletions src/v2/lens/mandatory_tag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,11 @@ import v2.extdeps.languages.dag {
// same-path shadow module is unwritable upstream of this gate. Grain: root - one rooted whole-tree
// walk locating dag_surface_module wrappers; per-module work is a bounded read of one small
// declaration subtree, never a per-node subtree re-walk (the required_lens_grain_note O(n^2) bar).
// Door grain (validate_then_compile / compile_source_root_ingest_with_admission) still
// refuses a trivial module at member_not_a_binder on the unmarked QN spine. That is
// not claimed green here (DESIGN §4b(1); review 77921). find_witness_reason_no_candidate
// is infer, before lenses, and is not inhabitance (DESIGN §3). The member-kind channel
// that would classify the spine is gunbc#13513.
// Corpus grain: the same fold is consumed at parse grain by the live witness in
// src/v2/test/claim/long/mandatory_tag_extdeps_corpus_test.dag over dag/extdeps/** via
// filesystem_list_dag_files + filesystem_read + the v2 grammar - the Node-tree projection that
Expand Down
28 changes: 21 additions & 7 deletions src/v2/lens/unit_modeling.dag
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,11 @@ import std.disposition { SingleAuthority }

import v2.std.witness { Holds }
import v2.std.node_query { edge_field_type_name, member_edge_type_node, member_not_a_binder_diagnostic }
import v2.extdeps.languages.dag {
dag_edge_is_module_surface_parse_projection,
dag_node_is_namespace_member_target,
dag_node_is_record_field_carrier
}
import v2.std.diagnostic { node_locus, outcome_accepted, outcome_rejected }
import std.optional { optional_absent, optional_present, optional_prefer_first_present }

Expand Down Expand Up @@ -95,8 +100,16 @@ fn type_is_flat_scalar(target: Node) -> Bool {
fn field_unit_violation(carrier: Node, edge: Edge) -> Optional<Diagnostic> {
match edge.label {
Authored { name: nm } =>
if dag_edge_is_module_surface_parse_projection(carrier: carrier, name: nm) {
optional_absent()
} else {
match member_edge_type_node(e: edge) {
Absent => optional_present(value: member_not_a_binder_diagnostic(e: edge))
Absent =>
if dag_node_is_namespace_member_target(node: edge.target) {
optional_absent()
} else {
optional_present(value: member_not_a_binder_diagnostic(e: edge))
}
Present { value: t } =>
if type_is_flat_scalar(target: t) {
if name_is_exempt(name: nm) {
Expand All @@ -108,18 +121,19 @@ fn field_unit_violation(carrier: Node, edge: Edge) -> Optional<Diagnostic> {
optional_absent()
}
}
}
StructuralLabel { label: _ } => optional_absent()
Positional => optional_absent()
}
}

fn carrier_first_unit_violation(carrier: Node) -> Optional<Diagnostic> {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_unit_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
if dag_node_is_record_field_carrier(node: carrier) {
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_unit_violation(carrier: carrier, edge: edge))
})
} else {
optional_absent()
}
}

Expand Down
8 changes: 5 additions & 3 deletions src/v2/test/claim/advisories/fatal_first_readers_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -66,9 +66,11 @@ test fn grammar_coverage_stage_rejected_reports_each_chains_fatal_holds() -> Boo
}

// THE DOOR LEDGER'S HISTOGRAM IS OF FATAL CAUSES. The three refusal chains the long claim
// v2.test.long.compile_door_ledger's real subjects produce (determinism, error_primitives, bit) are
// SUPPLIED here, each headed by one shared advisory: the histogram must count their fatals, and every
// fatal must be owned. A head-grain reader counts the advisory three times and nothing else.
// v2.test.long.compile_door_ledger's real subjects historically produced (determinism,
// error_primitives, bit) are SUPPLIED here, each headed by one shared advisory: the histogram
// must count their fatals, and every fatal must be owned. A head-grain reader counts the
// advisory three times and nothing else. Do not substitute unrelated causes for
// member_not_a_binder on error_primitives/bit.
test fn door_ledger_histogram_counts_each_refusals_fatal_holds() -> Bool {
let rows = [
door_refused_row(path: "dag/std/determinism.dag", d: residue_headed_chain(fatal: ^resolve_reason_unbound_symbol)),
Expand Down
Original file line number Diff line number Diff line change
@@ -1,17 +1,28 @@
module v2.test.lens_lifecycle_carrier.raw_prose_field_flagged

import std.occurrence_identity { OccurrenceSynthetic }
import v2.compiler.compile {
lifecycle_carrier_lens,
run_required_lens_gates_on_subtree
}
import v2.compiler.infer { InferredTree }
import v2.lens.lifecycle_carrier { lifecycle_carrier_gate }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.node {
Atom,
Arrow,
Conj,
Edge,
Authored,
Node,
Positional,
Symbol,
TypeNode,
}
import v2.test.lens_common.infer_fixture {
claim_inferred_facts,
claim_inferred_tree
}
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import v2.std.node_query { binder_edge }

Expand Down Expand Up @@ -112,3 +123,56 @@ test fn ordinary_string_field_is_accepted() -> Bool {
Rejected { diagnostics: _ } => false
}
}

// RED (parameter domain): fn f(dissolve_on: String) -> Int. The domain Conj is a record
// carrier; fold_node must still reach it under the Arrow (not stop at Arrow).
data arrow_param_domain: Node = Node {
kind: TypeNode { connective: Conj },
children: [
binder_edge(name: ^dissolve_on, type_node: string_leaf_target)
],
occurrence_id: OccurrenceSynthetic
}

data arrow_param_codomain: Node = Node {
kind: TypeNode { connective: Atom { identity: ^Int } },
children: [],
occurrence_id: OccurrenceSynthetic
}

data arrow_with_dissolve_on_param: Node = Node {
kind: TypeNode { connective: Arrow },
children: [
Edge { label: Positional, target: arrow_param_domain },
Edge { label: Positional, target: arrow_param_codomain }
],
occurrence_id: OccurrenceSynthetic
}

fn arrow_param_tree() -> InferredTree {
claim_inferred_tree(
root: arrow_with_dissolve_on_param,
facts: claim_inferred_facts(
type_symbol: ^arrow_param_type_sym,
algebra_symbol: ^arrow_param_algebra_sym,
descent_symbol: ^arrow_param_descent_sym
)
)
}

test fn arrow_parameter_dissolve_on_string_is_rejected_on_the_domain() -> Bool {
match lifecycle_carrier_gate(node: arrow_param_domain) {
Rejected { diagnostics: r } => r.head.reason == ^lifecycle_carrier_raw_prose_field
Accepted { value: _, diagnostics: _ } => false
}
}

test fn subtree_walk_reaches_arrow_parameter_dissolve_on() -> Bool {
match run_required_lens_gates_on_subtree(
inferred: arrow_param_tree(),
lenses: [lifecycle_carrier_lens]
) {
Rejected { diagnostics: r } => r.head.reason == ^lifecycle_carrier_raw_prose_field
Accepted { value: _, diagnostics: _ } => false
}
}
Loading
Loading