The FreeMonoid match lowering answers every arm, at any spine depth, or refuses

dag/gunbc/instruments/e0599_emitter_decision_census.dag

@@ -169,8 +169,8 @@ data e0599_lowering_rows: List<E0599LoweringRow> = [
     operation: FreeMonoidEmptyTest,
     ownership_alternative: "NotApplicable - a read; no copy is requested and no ownership predicate gates it",
     source_construct: "match over the FreeMonoid coproduct — the Empty/Cons discrimination itself",
-    emitter_authority: "v1.compiler.emit_rust emit_native_freemonoid_match | emit_native_freemonoid_tco_match",
-    emitted_literal: "{ let __fm = <scrut>; if __fm.is_empty() { .. } else { .. } }",
+    emitter_authority: "v1.compiler.emit_rust emit_native_freemonoid_match | emit_native_freemonoid_tco_match | fm_spine_condition",
+    emitted_literal: "{ let __fm = <scrut>; if __fm.is_empty() { .. } else if __fm.len() == <n> { .. } else { .. } }",
     cause: TargetApiRequirement,
     required_trait: "Clone",
     authority: e0599_im_vector_inherent_impl,
@@ -180,8 +180,8 @@ data e0599_lowering_rows: List<E0599LoweringRow> = [
     operation: FreeMonoidTailIterate,
     ownership_alternative: "NotApplicable - a read; no copy is requested and no ownership predicate gates it",
     source_construct: "match over the FreeMonoid coproduct — the Cons { tail } binding",
-    emitter_authority: "v1.compiler.emit_rust freemonoid_tail_let_from_fm",
-    emitted_literal: "let <tail>: Rc<Vec<_>> = Rc::new(__fm.skip(1)); ",
+    emitter_authority: "v1.compiler.emit_rust fm_spine_binds",
+    emitted_literal: "let <tail>: Rc<Vec<_>> = Rc::new(__fm.skip(<depth>)); ",
     cause: TargetApiRequirement,
     required_trait: "Clone",
     authority: e0599_im_vector_inherent_impl,
@@ -191,18 +191,18 @@ data e0599_lowering_rows: List<E0599LoweringRow> = [
     operation: FreeMonoidHeadExtract,
     ownership_alternative: "NotApplicable - no move or borrow exists out of shared storage; the owned element must be materialized",
     source_construct: "match over the FreeMonoid coproduct — the Cons { head } binding",
-    emitter_authority: "v1.compiler.emit_rust freemonoid_nonempty_branch_body | freemonoid_tco_nonempty_branch_body",
-    emitted_literal: "let <head> = (*__fm)[0].clone(); ",
+    emitter_authority: "v1.compiler.emit_rust fm_head_bind_lets",
+    emitted_literal: "let <head> = (*__fm)[<i>].clone(); ",
     cause: OwnedDeconstructionRequirement,
     required_trait: "Clone",
     authority: e0599_im_vector_index_impl,
     rationale: "The source binds Cons { head } by value, so an owned element must be materialized out of shared storage; you cannot move element 0 out of an Rc<Vector<T>>. Real given the representation, and not an ownership defect: no move or borrow was available to take instead.",
   },
   E0599LoweringRow {
     operation: FreeMonoidCatchallBind,
-    ownership_alternative: "NoEmitterArm - the bind is unconditional in v1.compiler.emit_rust freemonoid_empty_branch_body | freemonoid_nonempty_branch_body | freemonoid_tco_empty_branch_body | freemonoid_tco_nonempty_branch_body (row is uninhabited in the B0 measurement)",
+    ownership_alternative: "NoEmitterArm - the bind is unconditional in v1.compiler.emit_rust fm_spine_binds (row is uninhabited in the B0 measurement)",
     source_construct: "match over the FreeMonoid coproduct — a catch-all arm binding the whole scrutinee",
-    emitter_authority: "v1.compiler.emit_rust freemonoid_empty_branch_body | freemonoid_nonempty_branch_body | freemonoid_tco_empty_branch_body | freemonoid_tco_nonempty_branch_body",
+    emitter_authority: "v1.compiler.emit_rust fm_spine_binds",
     emitted_literal: "let <bind> = __fm.clone(); ",
     cause: CloneSharedRequirement,
     required_trait: "Clone",

dag/gunbc/recurring_failure_mode/special_cased_lowering_answers_a_narrower_question_than_its_arms_ask.dag

@@ -0,0 +1,38 @@
+module gunbc.recurring_failure_mode.special_cased_lowering_answers_a_narrower_question_than_its_arms_ask
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data special_cased_lowering_answers_a_narrower_question_than_its_arms_ask: RecurringFailureMode = RecurringFailureMode {
+  identity: "special_cased_lowering_answers_a_narrower_question_than_its_arms_ask" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: a target-specific lowering is admitted by a predicate that establishes the SHAPE OF THE SCRUTINEE and not the shape of the ARMS, so it runs over arm sets it cannot express and silently answers a narrower question -- selecting a branch the source never selects, and discarding arms it never read. The emitted program compiles, runs, and returns a well-typed wrong value.",
+
+    "HARM: DESIGN section 5's fabricated plausible output, at the one layer where no gate is watching. It is NOT the ordinary emitter-defect class: `guarded_filter_branch_dropped_by_emitter` publishes a TRUNCATED FILE, and `accepted_source_emits_uncompilable_target` publishes a file rustc refuses. Both leave an artifact that is wrong in a way SOMETHING can read. This class publishes an artifact that is complete, compilable, idiomatic, and semantically different from the source -- there is no missing symbol to grep for and no diagnostic to count.",
+
+    "THE DISTINGUISHING FACT, AND IT IS WHY THE WHOLE WITNESS FLOOR IS BLIND TO IT: the INTERPRETER lowers these arm sets correctly. Interpretation and emission are two paths from one source (DESIGN section 4b(1): a class's rung is the MINIMUM across its in-scope paths), and every enrolled claim runs the interpreter. So a claim over the defective function is green, its assertion is true, and the emitted binary answers differently -- the divergence is invisible to the entire enrolled corpus BY CONSTRUCTION, not by omission. A green claim_run is not merely weak evidence here; it is evidence about the other path. Only a control that RUNS EMITTED can discriminate.",
+
+    "RECEIPT (gunbc, 2026-09-22, found by witty-cat-84 on Pkg12, EXECUTED rather than read). `v1.compiler.emit_rust` lowered a FreeMonoid match by asking two questions -- which arm mentions `Empty`, which arm mentions `Cons` -- keeping the FIRST answer to each and emitting `if __fm.is_empty() { A } else { B }`. Its admission predicate `arms_are_freemonoid_coproduct` asked only whether the arms resolve to FreeMonoid; it never asked whether they FIT a two-way split. Two consequences, both silent: a REFUTABLE field sub-pattern degraded to a wildcard, because the binding reader returned \"_\" for anything that was not a `Bind`; and every arm after the first `Cons` arm was discarded, because nothing read past `first`. An arm GUARD was dropped on the same reasoning -- no branch body ever read `arm_guard`.",
+
+    "THE MEASURED SPECIMEN: `v2.std.algebra` `list_init` -- `Empty => Empty | Cons { head: _, tail: Empty } => Empty | Cons { head: h, tail: t } => Cons { head: h, tail: list_init(xs: t) }` -- emitted as `if __fm.is_empty() { vec![] } else { vec![] }`. In the emitted binary `qualified_name_init([\"v2\", \"acp_user\", \"acp_row\"])` returned `[]` instead of `[\"v2\", \"acp_user\"]`, so the native resolver's ancestor walk in `symbol_index_lexical_collect` skipped EVERY intermediate ancestor. That is why the native route could not resolve a module-level name from inside a declaration body; a global-bare fallback tier was answering those lookups and masking it, so the dead chain cost nothing observable until the fallback was removed.",
+
+    "THE SECOND INSTANCE MAKES THE CLASS RATHER THAN THE SITE: `v2.lens.cost.copied_port_derivation` -- `Empty => Absent | Cons { head: only, tail: Empty } => Present | _ => Absent` -- emitted as `if is_empty { None } else { Some(first) }`, reporting \"exactly one\" for a three-element list. Same lowering, different module, different consequence: one silently truncates a list, the other silently widens a cardinality claim. A per-site repair at either would have left the other standing, which is the tell that the defect is in the RULE.",
+
+    "RECOGNITION RULE: an admission predicate and the lowering it admits must range over the SAME facts. If the predicate reads the scrutinee's type and the lowering reads the arms' structure, there is an unstated premise between them -- that the arms have the shape the lowering can express -- and an unstated premise is where this class lives. The mechanical tell is a lowering that reaches its arms through `first` or a by-name lookup instead of folding all of them: `first` is a decision that the rest do not matter, made without looking.",
+
+    "REPAIR, AT THE RULE AND FOR THE CLASS: the lowering derives, per arm, a decidable predicate over the SAME facts the admission asked about -- for a FreeMonoid spine, an exact length or a length floor plus indexed head reads at any depth -- and emits the arms as an ordered chain of those predicates, which is what a match MEANS. Exhaustiveness is decided on those same facts, so the chain's final `else` is proven total rather than assumed, and no `unreachable!` stands in for the proof. Every shape the analysis cannot express -- an arm guard, a refutable `head` sub-pattern, a variant that is neither `Empty` nor `Cons`, an arm set not provably exhaustive -- emits a located `compile_error!` naming the shape and its span. The failure arm REFUSES; it does not widen (DESIGN section 5, absorbing fallback).",
+
+    "SELF-HOSTING HAZARD THE REPAIR HAD TO CLEAR, recorded because it recurs for any defect in the seed's own emitter: `v1.compiler.emit_rust` is EMITTED BY THE SEED IT FIXES, so a repair authored in the very shape the old lowering breaks would be miscompiled into the regenerated mirror, and the fixed point would take two regeneration rounds with a miscompiled emitter in between. The repair is therefore written so that no new function uses the broken shape -- the spine recursion tests the tail's `count` rather than matching `tail: Empty` -- and ONE round reaches the fixed point. Check this before authoring any emitter repair: the shape you are fixing is a shape you may not use.",
+
+    "RUNG FOUND AT: outside the ladder. The state was writable, accepted, emitted, executed, and silent, with no diagnostic anywhere and no enrolled claim able to go red.",
+
+    "ATTAINABLE CEILING: 3, structurally guaranteed, and the reason it is not 4 is that a target-specific lowering is a legitimate and necessary construct -- a FreeMonoid is realized as a host vector and a native length decision is the correct realization of it -- so the PAIRING of a lowering with an admission predicate remains writable and a future pair can be mis-scoped exactly this way. What is achievable is that no such pair can be ACCEPTED while it reaches its arms non-totally: a lowering either folds every arm or refuses, derived from structure rather than checked after the fact. The repair above reaches that rung for this one lowering and does not reach it for the class.",
+
+    "RUNG FOUND AT, CORRECTED. An earlier revision of this row said the enrolled floor STRUCTURALLY COULD NOT supply discriminating evidence for this class, `because every claim it runs is interpreted`. That was a SUBJECT CONFLATION and it is retracted here rather than softened. It is true of the defect's CONSEQUENCE -- a miscompiled binary answering wrongly at runtime, which no interpreted claim reaches -- and FALSE of the repair's own SUBJECT: the lowering is a pure String fold, so the arms it emits and the refusals it raises are decidable by an interpreted claim over a fixture handed to the compiler. DESIGN section 4b says so directly: a state unrepresentable in the accepted corpus may still be representable as SOURCE HANDED TO THE COMPILER BY A FIXTURE, and where the refusal is authorable there the evidence is enrollable there and declining it is specification-without-execution. The harder question was used to excuse not asking the easy one, which parked an available climb behind a capability that does not need to exist -- the section 4b(2) failure of reporting `can climb now but unbuilt` as `cannot climb further`. Found by review 69861 on gunbc#12026, not by this lane. The evidence is now enrolled as test.claim.emitter_freemonoid_arm_chain_witness_test: one discriminating red over the pre-repair shape, one positive control that the ordinary two-arm shape still lowers natively, and two refusal controls (refutable head sub-pattern, guarded arm) so the refusal arm cannot be satisfied by refusing everything.",
+
+    "NEXT-RUNG TRIGGER, NAMED AS THE CAPABILITY AND SCOPED TO WHAT IS ACTUALLY MISSING: an executed EMISSION-PATH differential oracle -- the same source evaluated by the interpreter and by the EMITTED BINARY over the same inputs, with a disagreement reported as a located refusal. That is the residue the enrolled rows above genuinely cannot reach, because they assert EMITTED TEXT and no enrolled claim executes emitted code; the behavioural evidence for this repair (the emitted binary returning [1, 2] for list_init([1, 2, 3]) against the broken []) was measured by hand on gunbc#12026 and is reproducible only outside the floor. Scoped this narrowly on purpose: the earlier phrasing claimed the whole class was out of reach and was wrong about the larger half of it.",
+  ],
+
+  evidence: [],
+}