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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
module gunbc.recurring_failure_mode.shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element: RecurringFailureMode = RecurringFailureMode {
identity: "shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element" as NonEmptyStr,

receipts: [
"**A STRUCTURAL PREDICATE THAT INSPECTS ONLY THE FIRST CHILD CANNOT DISTINGUISH A CONTAINER OF N ELEMENTS FROM ONE ELEMENT, so the container is admitted AS an element and elements 2..N are silently dropped by whatever consumes the match.** The invalid state is a total, pure, fail-closed-looking walk that returns a population of the right TYPE and the wrong CARDINALITY, with no refusal anywhere: the consumer reads the accepted value's head, produces a well-formed partial answer, and reports Accepted. The harm is DESIGN section 5's forbidden case rather than a rung: a fabricated plausible output, here a syntactically valid target module missing most of its declarations, which compiles and therefore fails no downstream check either. ",

"**SPECIMEN WITH A RECEIPT, measured 2026-09-09 on the v2 production Rust door.** `v2.compiler.emit_produced` `produced_decl_node_is_decl` asked whether a node was a `Conj` whose FIRST child is a `Named` edge into an `Arrow`, and `produced_decl_conjs_in_tree` recorded such a node and stopped descending. But a resolved .dag module carries one `Named`-into-`Arrow` edge PER DECLARATION on a single shell `Conj`, so the SHELL satisfied that predicate; the walk recorded the shell as one declaration, and `emit_produced_decl` -- which reads `children[0]` -- emitted declaration 1 and dropped 2..N. Measured through `observe_provenanced_rust_emission_from_ingest` over an ingested two-declaration module: `ArtifactProduced`, carrying exactly the first declaration. Enrolled evidence: `v2.test.claim.self_host.rust_module_emission_population`, whose count arm read 1 before the repair and 2 after, one stage BEFORE emission so a correct concatenation could not stand in for a correct collection. ",

"**WHY IT SURVIVED, and this is the transferable part.** Every existing witness over the same fold was green throughout, because each one HANDED THE FOLD A LIST OF DECLARATIONS IT HAD BUILT ITSELF (`ingested_add_decl_node`, `table_fixture_add_decl_node`) and therefore never exercised the collector at all. A fixture that constructs the population cannot discriminate a defect in DERIVING the population, however thoroughly it pins the fold's ordering, separators and refusal propagation -- and the ordering witness in particular reads as if it covers exactly this. The specimen must be the real ingested tree. ",

"**THE COINCIDENCE THAT HID IT AND THE DEAD REFUSAL THAT LOOKED LIKE A WALL.** At N=1 the shell and the declaration ARE the same node, so the only shape the door was exercised on was correct by accident, and every byte-level golden agreed. Above it the composition carried an explicit surplus arm refusing `rust_module_emission_decl_ambiguous` -- which was UNREACHABLE from any real module, because the collector never produced a surplus to refuse. **A REFUSAL FOR THE CASE A DEFECTIVE PRODUCER CANNOT PRODUCE READS AS A WALL AND IS A DECORATION** (DESIGN section 4b: ask whether the check's RED is authorable before writing the check). The lane's premise was that this arm was the admission ceiling to relax; it was never load-bearing, and relaxing it alone would have published partial modules under a wider admission. ",

"**RECOGNITION RULE: when a predicate decides a node's ROLE, name the two roles it must separate and check whether both can present the same first child.** A container and its first element routinely can. The repair direction is to move the predicate onto the EDGE that actually carries the role -- here a declaration IS the named edge into an arrow, and no per-declaration node exists in the tree at all -- rather than to add a count or a depth guard to the node predicate, which re-states the same conflation with a bound on it. The field tell needs no execution: a SECOND private collector answering the same question nearby. `v2.workflow.realization_attempt` `collect_arrows` walked the shell's edges one-per-declaration and was correct; its existence beside this authority is the static symptom, and DESIGN section 3 already prices the fork. ",

"**RUNG FOUND AT: below the ladder -- silent wrongness, which section 4b states is not a rung. CURRENT RUNG AFTER REPAIR: 2 (mechanically preventable): the walk is correct and an executing discriminating RED holds it, but the invalid predicate remains writable and the guarantee depends on that witness staying enrolled. CEILING: 4 (structurally impossible), because whether a node's role predicate can be satisfied by a container of that role is decidable from declarations the Node tree already carries. NEXT-RUNG TRIGGER, a CAPABILITY and not an artifact: a structural role predicate declares the role it decides and the carrier that role inhabits, so a predicate whose match is satisfiable by a container of its own role fails to compile. That capability does not exist today (measured 2026-09-09: role predicates in the corpus are ordinary Bool functions over Node with no declared subject role), so this is a stall whose trigger is an absent language capability, not a scheduled edit.** ",
],

evidence: [],
}
102 changes: 58 additions & 44 deletions src/v2/compiler/emit_produced.dag
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ import v2.std.diagnostic {
node_locus,
outcome_rejected
}
import v2.std.node { Arrow, Conj, Edge, Named, Node, Positional, Symbol, TypeNode }
import v2.std.node { Arrow, Conj, Edge, Named, Node, node_synthetic, Positional, Symbol, TypeNode }
import v2.std.logic { Bool }
import v2.std.text { String }

Expand Down Expand Up @@ -70,38 +70,48 @@ fn emit_produced_decl_inner_arrow(decl: Node) -> Outcome<Node> {
}
}

// WHERE PRODUCED DECLARATIONS COME FROM. A produced declaration inside a resolved tree is the
// decl-shaped node itself: a Conj whose first child is a Named edge into an Arrow — exactly the
// shape emit_produced_decl_inner_arrow and produced_decl_subject_from_decl consume, so collection
// never synthesizes a wrapper node. The fold is total and pure: it reports every decl-shaped node
// and never recurses into one (a declaration owns its subtree). How many declarations a
// composition expects, and what a zero or surplus population means, is the caller's admission
// policy — never a silent filter here.
// The children match lives behind a declared FreeMonoid<Edge> parameter because the v1 seed
// stamps pattern variables from a declared parameter type, not from a field-access scrutinee:
// matching node.children directly leaves the Cons head as an unresolved T (no field 'label' on
// type 'T'), and routing the same lookup through list_at_optional fails its generic instantiation
// when the callee is typechecked lazily from inside the recursive collector cluster.
fn produced_decl_children_have_decl_head(children: FreeMonoid<Edge>) -> Bool {
match children {
Empty => false
Cons { head: first, tail: _ } =>
match first.label {
Named { name: _ } =>
match first.target.kind {
TypeNode { connective: Arrow } => true
_ => false
}
Positional => false
// WHERE PRODUCED DECLARATIONS COME FROM. A declaration in a resolved module is the NAMED EDGE
// INTO AN ARROW, never a node: the module shell is a Conj carrying one such edge per declaration,
// and no separate per-declaration node exists in the tree to collect. The previous walk looked for
// a decl-shaped NODE — a Conj whose FIRST child is a Named edge into an Arrow — and that predicate
// cannot tell an N-declaration shell from a 1-declaration one, because both have the same first
// child. So the shell itself matched, collection stopped there, and emission (which reads
// children[0]) published declaration 1 and SILENTLY DROPPED declarations 2..N. A one-declaration
// module was correct only by coincidence, shell and declaration being the same node at N=1.
// Measured on the production ingest path 2026-09-09: a two-declaration module emitted exactly its
// first declaration and reported Accepted.
// The walk is therefore edge-driven and total: descend an edge that is not a declaration, record
// one declaration per edge that is, and never descend INTO a declaration (an arrow body's inner
// named arrows are not module declarations). Order is source order. The single-edge Conj this
// projects per declaration is the declaration's canonical node form — the same shape
// v2.compiler.ingested_fixture_arrows ingested_add_decl_node builds — so emit_produced_decl and
// produced_decl_subject_from_decl keep consuming a Node.
// STANDING §3 FORK, NOT CLOSED HERE: v2.workflow.realization_attempt collect_arrows answers this
// same question for itself, and answered it CORRECTLY per-edge while this authority did not, which
// is why the census lane never saw the drop. Consolidating it onto this collector is a separate
// change against a separate consumer (it walks a RESOLVED tree and searches for the first arrow
// BELOW an edge rather than requiring the edge to target one), and merging the two without
// measuring that difference would trade a silent drop for a silent empty population.
// How many declarations a composition expects, and what an empty population means, is the
// caller's admission policy — never a silent filter here.
// The label/kind match lives behind a declared Edge parameter because the v1 seed stamps pattern
// variables from a declared parameter type, not from a field-access scrutinee.
fn produced_decl_edge_is_decl(edge: Edge) -> Bool {
match edge.label {
Named { name: _ } =>
match edge.target.kind {
TypeNode { connective: Arrow } => true
_ => false
}
Positional => false
}
}

fn produced_decl_node_is_decl(node: Node) -> Bool {
match node.kind {
TypeNode { connective: Conj } => produced_decl_children_have_decl_head(children: node.children)
_ => false
}
fn produced_decl_node_for_edge(edge: Edge) -> Node {
node_synthetic(
kind: TypeNode { connective: Conj },
children: [edge]
)
}

fn produced_decl_conjs_in_children(
Expand All @@ -113,21 +123,17 @@ fn produced_decl_conjs_in_children(
Cons { head: e, tail: rest } =>
produced_decl_conjs_in_children(
children: rest,
acc: produced_decl_conjs_in_tree_into(node: e.target, acc: acc)
acc: if produced_decl_edge_is_decl(edge: e) {
list_snoc_item(xs: acc, item: produced_decl_node_for_edge(edge: e))
} else {
produced_decl_conjs_in_children(children: e.target.children, acc: acc)
}
)
}
}

fn produced_decl_conjs_in_tree_into(node: Node, acc: FreeMonoid<Node>) -> FreeMonoid<Node> {
if produced_decl_node_is_decl(node: node) {
list_snoc_item(xs: acc, item: node)
} else {
produced_decl_conjs_in_children(children: node.children, acc: acc)
}
}

fn produced_decl_conjs_in_tree(root: Node) -> FreeMonoid<Node> {
produced_decl_conjs_in_tree_into(node: root, acc: Empty)
produced_decl_conjs_in_children(children: root.children, acc: Empty)
}

fn emit_produced_decl_with_target(
Expand Down Expand Up @@ -191,10 +197,7 @@ fn emit_produced_module_append(
o: emit_produced_decl(decl: decl, target: target),
f: fn(medium) {
Accepted {
value: list_append(
left: list_append(left: partial, right: medium.carried),
right: emit_module_decl_separator
),
value: concat(partial, medium.carried, emit_module_decl_separator),
diagnostics: None
}
}
Expand All @@ -214,11 +217,22 @@ fn emit_produced_module_step(
)
}

// THE JOIN IS `concat` OVER A "" SEED, NOT `list_append` OVER `Empty`, and the difference is not
// cosmetic. Built by list_append from the FreeMonoid variant, the fold's result carries the
// CONS-LIST SPELLING of a string rather than the native one: `==` and `concat` still behave, which
// is why every golden over this fold stayed green for as long as goldens were all that read it --
// but a builtin that requires a native string REFUSES it. Measured 2026-09-10 as `split expects a
// string, got Variant` from v2.test.self_host.stage0_production_target's two contains-controls,
// the first consumers to read this fold's output through `split`. Nothing on the production door
// reached this fold until the door started routing every nonempty population through it, so the
// defect was latent rather than new, and the equality-only readers could never have found it.
// One representation for one concept (DESIGN section 3): a String is a String, not a FreeMonoid
// that happens to compare equal to one.
fn emit_produced_module(decls: List<Node>, target: TargetModel) -> Outcome<Medium<String>> {
bind_outcome(
o: fold_list(
xs: decls,
empty: Accepted { value: Empty, diagnostics: None },
empty: Accepted { value: "", diagnostics: None },
cons: fn(acc, decl) { emit_produced_module_step(acc: acc, decl: decl, target: target) }
),
f: fn(joined) { target_source_medium(text: joined, target: target) }
Expand Down
59 changes: 30 additions & 29 deletions src/v2/compiler/self_host/candidate_generation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module v2.compiler.self_host.candidate_generation
import extdeps.communication.medium { Medium }
import extdeps.filesystem.filesystem_io { Filesystem }
import v2.compiler.emit { emit }
import v2.compiler.emit_produced { emit_produced_decl, produced_decl_conjs_in_tree }
import v2.compiler.emit_produced { emit_produced_module, produced_decl_conjs_in_tree }
import v2.compiler.infer { infer, InferredTree }
import v2.compiler.name_resolve { Admission }
import v2.compiler.program_assembly { assemble_program_from_ingest }
Expand Down Expand Up @@ -176,17 +176,29 @@ fn generate_rust_emission_candidate(
)
}

// The production module composition. Admission is exactly one produced-decl-shaped node (the
// collector in v2.compiler.emit_produced defines the shape): the door's specimen class is the
// single-declaration module, and zero or surplus populations refuse typed and located rather than
// picking a winner. The multi-declaration join convention lands with the first multi-declaration
// consumer — emit_produced_module's trailing separator is pinned by its own goldens and is not
// this composition's fact.
// The production module composition. Admission is the collector's ORDERED declaration population
// (v2.compiler.emit_produced produced_decl_conjs_in_tree defines what a declaration is and stops
// at one, so structure inside a body is never a top-level declaration). An empty population
// refuses typed and located; every nonempty population — one declaration or many — goes through
// the one module authority, emit_produced_module, whose fold propagates the first refusal rather
// than publishing a partial module.
// THE EXACTLY-ONE CEILING THIS REPLACES WAS NOT THE WALL IT READ AS, and saying why is the point:
// its surplus arm refused ^rust_module_emission_decl_ambiguous for a second declaration, and that
// arm was UNREACHABLE from any real ingested module, because the collector beneath it reported a
// whole N-declaration module shell as ONE declaration and emission published only the first. So
// the door was not refusing multi-declaration modules; it was silently truncating them, and
// relaxing this admission alone would have widened that. The collector is repaired in the same
// change and the class is filed at
// gunbc.recurring_failure_mode.shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element.
// The trailing separator is emit_produced_module's declared convention — the same one
// v2.compiler.emit_module emit_module_decl_separator applies to every declaration including the
// last — so a one-declaration module ends with it too.
fn generate_rust_module_emission_candidate(
inferred: InferredTree,
target: TargetModel
) -> Outcome<RustEmissionCandidate> {
match produced_decl_conjs_in_tree(root: inferred.root) {
let decls = produced_decl_conjs_in_tree(root: inferred.root)
match decls {
Empty =>
outcome_rejected(
d: Diagnostic {
Expand All @@ -195,29 +207,18 @@ fn generate_rust_module_emission_candidate(
correction: Unavailable { reason: ExternalContractUnknown }
}
)
Cons { head: decl, tail: rest } =>
match rest {
Empty =>
bind_outcome(
o: emit_produced_decl(decl: decl, target: target),
f: fn(source) {
outcome_accepted(
value: RustEmissionCandidate {
source: source,
emitted: inferred.root
}
)
}
)
Cons { head: surplus, tail: _ } =>
outcome_rejected(
d: Diagnostic {
reason: ^rust_module_emission_decl_ambiguous,
at: node_locus(node: surplus),
correction: Unavailable { reason: ExternalContractUnknown }
Cons { head: _, tail: _ } =>
bind_outcome(
o: emit_produced_module(decls: decls, target: target),
f: fn(source) {
outcome_accepted(
value: RustEmissionCandidate {
source: source,
emitted: inferred.root
}
)
}
}
)
}
}

Expand Down
8 changes: 7 additions & 1 deletion src/v2/compiler/self_host/direct_rust_door_fixture.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module v2.compiler.self_host.direct_rust_door_fixture

import extdeps.communication.medium { Lossless, Medium }
import v2.compiler.emit_module { emit_module_decl_separator }
import v2.compiler.infer { DerivedGrounding, InferredFacts, InferredTree, infer }
import v2.compiler.program_assembly { assemble_program_from_ingest }
import v2.extdeps.languages.dag { dag_language_model }
Expand Down Expand Up @@ -61,7 +62,12 @@ import v2.std.witness {

data direct_rust_door_module_path: String = "src/v2/compiler/self_host/direct_rust_door_fixture.dag"

data direct_rust_door_expected_source: String = rust_source_text
// The door emits a MODULE, so the expected source is the declaration text followed by the module
// authority's declared declaration separator — the same convention emit_produced_module and
// emit_module apply to every declaration including the last. It is composed from the two
// authorities rather than transcribed, so a change to either is a located red here, not a silent
// drift between a literal and the emitter that produces it.
data direct_rust_door_expected_source: String = concat(rust_source_text, emit_module_decl_separator)

data direct_rust_door_dag_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n"

Expand Down
Loading
Loading