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

[gunbai-bot]

Subject

v1.compiler.emit_rust's FreeMonoid match lowering. A nested constructor pattern in a field position was dropped and every arm after it discarded, so the emitted program compiled, ran, and returned a well-typed wrong value. DESIGN §5 fabricated plausible output, which is outside the guarantee ladder rather than low on it.

Found by witty-cat-84 (Pkg12), executed rather than read. Pkg12's native census was blocked on this.

The defect, and it is in the rule

emit_native_freemonoid_match asked two questions — which arm mentions Empty, which arm mentions Cons — kept the first answer to each, and emitted if __fm.is_empty() { A } else { B }. Its admission predicate arms_are_freemonoid_coproduct established only that the arms resolve to FreeMonoid; it never asked whether they fit a two-way split.

Three silent consequences — the third was not in either report:

1. a refutable field sub-pattern degraded to a wildcard, because the binding reader returned "_" for anything that was not a Bind, so Cons { head: _, tail: Empty } matched every non-empty list;
2. every arm after the first Cons arm was discarded, because nothing read past first;
3. an arm guard was dropped outright, because no branch body ever read arm_guard.

Two sites, two different consequences — which is what makes this a defect in the rule rather than at either site. A per-site repair at either would have left the other standing.

• v2.std.algebra list_init emitted as if __fm.is_empty() { vec![] } else { vec![] }, so qualified_name_init(["v2","acp_user","acp_row"]) returned [] instead of ["v2","acp_user"] and the native resolver's ancestor walk skipped every intermediate ancestor. A global-bare fallback tier was masking it.
• v2.lens.cost.copied_port_derivation reports "exactly one" for a three-element list.

The construction

A FreeMonoid pattern is a spine of Cons levels terminating either in Empty (an exact length) or in a binding/wildcard tail (a length floor). So each arm carries a decidable length predicate and its head bindings are decidable index reads at any depth. The arms become an ordered chain of those predicates, which is what a match means. Exhaustiveness is decided on the same facts, so the chain's final else is proven total rather than assumed and no unreachable! is fabricated to stand in for the proof.

The TCO twin carried the identical defect and now shares the analysis, refusal and chain, with the body emitter the only variance.

Refusal, not widening (§5 absorbing fallback)

Shapes the analysis cannot express emit a located compile_error! naming the shape and span: an arm guard; a refutable head sub-pattern (a question about the element, not the list); a variant that is neither Empty nor Cons; an arm set not provably exhaustive.

The refusal arm is justified by construction, not by what the generic fallback would have done. I make no claim about the generic path's behaviour on a FreeMonoid match, because I did not run it.

Controls — all executed against EMITTED code

The interpreter lowers these arm sets correctly, so no interpreted claim can discriminate this fix; a green claim_run is evidence about the other path. Every row below ran the emitted binary.

The second specimen — the control the brief named and I had missed

v2.lens.cost.copied_port_derivation is Empty => Absent | Cons { head: only, tail: Empty } => Present | _ => Absent. Pre-repair it emitted if is_empty { None } else { Some(first) } — Present for a list of any non-zero length.

	list_init	copied_port_derivation
pre-repair answer	[] for every input	Some(first) for any non-empty
consequence	silently truncates a list	silently widens a cardinality claim

Same lowering, opposite consequences — which is the argument that the repair belongs at the rule. A per-site fix at either would have left the other standing.

It also shows why a two-way split cannot be patched into correctness: if is_empty { A } else { B } has nowhere to distinguish 1 from 3. The discrimination has to be the chain.

Verified at both halves. The real site is in the emitted 00_compile closure:

// pre-repair — cannot tell 1 from 3
if __fm.is_empty() { None } else { let only = (*__fm)[0].clone(); Some(only.clone()) }
// repaired — 0 → Absent, 1 → Present, 3 → Absent
if __fm.is_empty() { None } else if __fm.len() == 1 { let only = (*__fm)[0].clone(); Some(only.clone()) } else { None }

How it was missed: the brief's item 2 named three controls on the real emitted crate. I measured two and carried the third in the PR narrative without ever testing it. Found by re-reading the assignment against the diff after the approval landed — a reviewer reads the diff, not the brief, so this was never theirs to catch. An approval means "no blocking defect found", which is a different question from "does this do what was asked".

assertion	baseline (old lowering)	fixed
list_init([])	PASS	PASS
list_init([1])	PASS (accidentally — old lowering returns [] for everything)	PASS
list_init([1,2])	FAIL []	PASS [1]
list_init([1,2,3])	FAIL []	PASS [1,2]
qualified_name_init([v2,acp_user,acp_row])	FAIL []	PASS ["v2","acp_user"]
exit	1	0

Three discriminating assertions, not five. Rows 1–2 pass in both arms and are not evidence.

Artifact-level control, same closure:

// baseline
{ let __fm = xs.clone(); if __fm.is_empty() { Rc::new(vec![]) } else { Rc::new(vec![]) } }
// fixed
{ let __fm = xs.clone(); if __fm.is_empty() { Rc::new(vec![]) }
  else if __fm.len() == 1 { Rc::new(vec![]) }
  else { let h = (*__fm)[0].clone(); let t: Rc<Vec<_>> = Rc::new(__fm.skip(1)); ... } }

__fm.len() conditions across the closure: 0 baseline → 13 fixed.

Census — both emitted closures

closure	files	FM matches	refusals	blocking errors
src/v2/compiler/00_compile.dag	193	58	0	0
src/v2/cli/compile_cli.dag	171	53	0	0

Nothing in the emitted population hits a shape the analysis refuses, so no site that compiles today goes red.

A corpus-wide static census (381 Cons pattern arms, 112 files) finds 13 sites carrying a refusable shape — 12 refutable head: sub-patterns and the guarded arm in v2.workflow.floor_cost_debt_edit. All sit outside both emitted closures. Those sites are being silently mis-lowered today wherever something emits them; this change converts that silence into a refusal. Stated as a lower bound: the static census is regex over the corpus at rest, not the emitter's own walk.

Self-hosting hazard, cleared by measurement

This module is emitted by the seed it fixes, so a repair authored in the broken shape would be miscompiled into the regenerated mirror. The repair therefore avoids the shape it repairs — the spine recursion tests the tail's count rather than matching tail: Empty. Verified by reading the regenerated mirror: the old emitter lowered fm_chain_from correctly, both arms intact, so one regen round reaches the fixed point instead of two with a miscompiled emitter in between.

Fixed point — proven, not assumed

The committed mirror was produced by the old emitter (correct for bootstrapping), which leaves open whether the fixed emitter emits emit_rust identically. Two --required-regen rounds settle it:

round	emitter	drift reported
1	old	std_measure.rs, v1_compiler_emit_rust.rs
2	fixed	std_measure.rs only

v1_compiler_emit_rust.rs falling out of the list is the proof: the committed mirror is what the fixed emitter produces. std_measure.rs persists identically across both arms, independently confirming it is #11992's drift rather than anything this change touches.

Round 2 nearly ran with a stale claim_executor still carrying the old emitter, which would have reported a fixed point that meant nothing — the same shape as the bug being fixed here, an instrument giving a confident answer about the wrong subject. Caught by checking the binary's contents (strings | grep 'will not lower'), not its timestamp.

Disposition of what it replaces

Deleted, not left standing beside the new path: freemonoid_cons_binding, freemonoid_tail_let_from_fm, freemonoid_catchall_bind_name, and the four branch-body functions. The im::Vector::skip reasoning is preserved on fm_tail_bind_let, now skipping by the arm's own spine depth rather than always by one.

Bounded gaps, stated rather than papered over

• The self-host build cannot be shown green, and not because of this change. Main's is already broken by a separate emitter gap — base16's UInt8 cross-module alias, owned by wise-raven-686. Confirmed pre-existing by execution: emitting the same closure with the emitter reverted produces the same missing use-line. My probe only ran because I stubbed that module in /tmp only; nothing under version control is touched.
• std_measure.rs drift on main is not mine. required-regen reports it from 132c780e4a6 (FABRIC-MEM-GRANT-0: one memory grant carrier, one microVM sizing policy, one grain-parameterised rounder (reconciles #11883 + #11885) #11992) landing the grain-rounder .dag without its mirror. Deliberately excluded — folding it in would misrepresent this diff.
• Landing order settled with wise-raven-686: this lands first, they regenerate v1_compiler_emit_rust.rs from the merged base.

Rework after review 69861, and the evidence re-taken

Both findings were correct and are fixed.

The refusal was an in-band sentinel. FmArmPlan { supported: Bool, reason: String } with "" meaning lowerable was the same protocol this change deletes one layer down, reintroduced one layer up. Now a coproduct — FmSpine { exact, len, head_binds, tail_bind } | FmUnsupportedArm { cause } — with a seven-variant FmLoweringRefusal and one message function. An unsupported arm now has no spine fields to misread, and the 1000000 bottom is an Int?. I did not reuse OperatorRealizationRefusal as the review suggested: that type is about operators, and sharing the spelling would be a §3 meaning fork rather than single authority.

No enrolled discriminating evidence, and the row declared the gap unbridgeable when it is not. That was mine, and it is retracted in the row rather than softened. A subject conflation: "every claim the floor runs is interpreted" is true of the defect's consequence (a miscompiled binary answering wrongly at runtime) and false of the repair's subject (a pure String fold, decidable by an interpreted claim over a fixture). §4b(2) names it exactly — "can climb now but unbuilt" reported as "cannot climb further".

Enrolled as test.claim.emitter_freemonoid_arm_chain_witness_test, all four rows execute and return true:

row	what it establishes
nested arm + successor reach the chain	the discriminating red
ordinary two-arm shape still lowers natively	the refusal is not over-firing
refutable head sub-pattern refuses	unsupported shape refuses, not mis-lowers
guarded arm refuses	the third consequence, in neither original report

The positive control is load-bearing: without it, "refuse everything" satisfies both refusal rows while destroying all real lowering.

Evidence re-taken after the rework, since it touched emit_native_freemonoid_match and every earlier behavioural claim described a superseded revision:

	pre-rework	post-rework
list_init	3-arm chain, len() == 1	identical
refusals in closure	0	0
__fm.len() conditions	13 (2/11)	13 (2/11)
probe	5/5, exit 0	5/5, exit 0
red control	3/5 FAIL, exit 1	3/5 FAIL, exit 1

Pure refactor — measured, not asserted.

CI: the red belonged to main, not this branch

Two failing checks, one real failure: witnesses is the aggregator and failed in 3s reporting compiler=success clippy=success floor=failure. The floor carried exactly one refusal — test.claim.mtcollins1_census_image_local_wet.the_rendered_program_runs_and_its_output_parses_by_real_execution.

Not mine, and established rather than assumed: that witness renders a POSIX shell script and asserts host_capture_bind, which the FreeMonoid lowering cannot reach. #12020 ("repairs the wet-lane regression from #11987") merged at 01:19Z, and git merge-base --is-ancestor put its commit in origin/main and not in this branch — 9 commits behind. Integrated by merge; not repaired here.

Instrument provenance, recorded because it nearly produced a false finding

/cargo-target is shared across worktrees and sessions. A neighbouring build of v1-compiler overwrote the binary between my verifying it carried the rework and my measuring with it. Two witness rows reported false, and a fixture emitted a textbook reproduction of the original bug — from a compiler that predated the fix.

Caught only because two greps of one file disagreed: the rework-only string counted 1 earlier and 0 later. Every measurement above was re-taken with a worktree-local CARGO_TARGET_DIR, verified by a string that exists only in the reworked code.

The red control needs no such check, and the reason is worth keeping: its artifact carries the two-way split and zero length-conditions, and witness row one establishes that the fixed emitter emits len() == 1 for that exact shape. The output identifies its own producer — which is stronger than "the binary was correct when I looked."

What the review floor found here, and why it is the same bug one layer up

Four findings across two reviews. All four were correct, and two were things I would have defended. They are recorded here rather than in a commit message because the pattern is worth more to the reviewer of the next change than the individual fixes are to this one.

Every one had the same shape: a surface that reads correct over a claim nobody re-derived.

finding	what it looked like	what it was
FmArmPlan { supported: Bool, reason: String }	a tidy plan record	the in-band sentinel this PR deletes, reintroduced one layer up
"the floor structurally cannot supply the red"	an honest ceiling	the hard question excusing the easy one (§4b(2))
census naming five deleted functions	a stale comment	citations that no longer resolve (§3)
a dead != "" on the admission path	harmless dead code	one value carrying two facts
"drop_last(" pinning the third arm	the row's coverage argument	a decoration that cannot go red

The last one is the one worth reading

Both callers tested if native_fm != "" over a lowering that can no longer return "". My reading was dead code, harmless. It was not, and the reason is exactly the defect this PR repairs.

That empty string never came from the lowering at that site. It came from the admission predicate's own else branch. So one value encoded two distinct facts —

• these arms are not a FreeMonoid coproduct, and
• the lowering declined

— with nothing downstream able to separate them. A future lowering that legitimately produced no text would have been indistinguishable from one that declined, and would have silently rerouted to the generic path.

That is the same class as the bug under repair: emit_native_freemonoid_match answered a narrower question than its arms asked, and looked right doing it. Here a single String answered a narrower question than its callers asked, and looked right doing it.

The repair is the construction, not the check: the callers branch on arms_are_freemonoid_coproduct directly, the lowering always answers, and the sentinel has no spelling left.

The lowering itself has not been challenged since the first review, where it was worked through by hand. Every finding has been about the evidence and citations around it — which is the floor doing its job, not a signal the change is unsound.

The fifth finding is the sharpest, because it was in the evidence added to fix the second

Review 70019 found that the discriminating red's third-arm pin, "drop_last(", cannot go red: drop_last is the fixture's own function, so the emitted module carries pub fn drop_last( however the match lowers. And the annotation named list_tail as that pin — a symbol appearing nowhere in the file. The row's stated coverage argument cited a wall that was never built.

§4b names it: "permanently green by construction, carrying no information, and worse than absent because it will be cited as coverage." It was cited as coverage — in that annotation, in this body, and in three status reports claiming four rows green.

The gap was real: a lowering keeping arms 1–2 and dropping arm 3 would emit __fm.len() == 1, carry pub fn drop_last(, and pass. That is the original defect in narrower form.

Replaced with pins read off the artifact, and red-ability measured rather than argued — v2.std.algebra list_init carries this fixture's exact arm shape, and its retained pre-repair emission has skip(1) at 0 and list_init(t at 0:

pin	pre-repair	repaired
__fm.len() == 1	0	1
Rc::new(__fm.skip(1))	0	1
drop_last(t.clone())	0	1

The annotation now also records that the two new pins are not equally strong: the skip spelling is generic (the old emitter emitted it 10 times in v2_std_algebra alone) and discriminates here only because the first Cons arm's tail is a nested Empty the old binding reader degraded to _. drop_last(t.clone()) is the unambiguous one.

The uncomfortable part, kept because it is the lesson: this row was added in response to a finding that I had claimed evidence without producing it. The replacement evidence had a hole of the same kind, and I reported it green four times before a reviewer read the assertion rather than the claim about it.

An observation this PR does not fix, recorded because it is evidence

--required-regen reports drift in std_measure.rs on this branch in both rounds. I reported that as a clean result — "round two drifts std_measure.rs alone" — reading it as another lane's known drift.

It is not noise. kibibyte_from_byte_size_floor is declared at dag/std/measure.dag:338 and consumed three times by gunbc.compute.host_capacity, and has 0 occurrences in main's mirror. That mirror does not converge, and a regeneration whose edited set contains no .dag reports a fixed point vacuously — regenerating nothing and comparing nothing.

Three lanes hit this today from three directions (crisp-dove-588, snappy-seal-19, and this one). A lane owns it; it is not repaired here. It is stated because a vacuous fixed point and a real one are spelled identically at the call site, and because filing it as "known drift" three times is how it stayed invisible.

Failure mode row

gunbc.recurring_failure_mode.special_cased_lowering_answers_a_narrower_question_than_its_arms_ask — filed as a new class after checking the existing emitter rows. guarded_filter_branch_dropped_by_emitter publishes a truncated file; accepted_source_emits_uncompilable_target publishes one rustc refuses. Both leave an artifact something can read. This one publishes a complete, compilable, idiomatic artifact that is semantically different from its source.

Rung found at: outside the ladder. Ceiling: 3. Next-rung trigger, named as the capability: an executed emission-path differential oracle — interpreter vs emitted binary over the same inputs, disagreement reported as a located refusal. That is what the enrolled witness floor structurally cannot supply, because every claim it runs is interpreted.

🤖 Generated with Claude Code

[gunbai-bot]

Correcting a merge-time obligation recorded on this PR's handoff, so nobody waits on a ping that cannot arrive.

The handoff states that wise-raven-686 is waiting to be pinged when this merges, so they can regenerate src/v1/stage0/src/v1_compiler_emit_rust.rs from the merged base, and warns that without the ping they would regenerate from a stale base. That landing-order agreement was real when it was made and is now void:

• There is no refs/heads/session/wise-raven-686 on origin. That lane was archived with its work unpushed — confirmed twice today, once when a peer manager asked whether anyone held that region unpushed.
• The base16 UInt8 work it owned was picked up and completed elsewhere, as base16 decodes into the sealed octet carrier; the forked-import use-line defect is filed with its control #12056 (session/sharp-bear-756). I checked that PR's file list: twelve .dag files under dag/, no 05_emit_rust.dag and no stage0 mirror at all. So it owes no regeneration against this merge and there is no stale-base hazard between them.

So: no ping is owed, and nothing is waiting on this merge from that direction. The mirror-ordering constraint that does still apply is between this PR, #12029 and #12034 — all three regenerate v1_compiler_emit_rust.rs from different bases, so they land one at a time with the later ones regenerating from the merged base. That is carried on the operator's merge card, and I own the regeneration if the queue reds.

The second obligation stands unchanged and needs no action here: witty-cat-84's Pkg12 native census unblocks on this merge (session/witty-cat-84 is live). They found this defect; qualified_name_init now returns [v2, acp_user] instead of [].

Also preserved from the handoff, because these are the parts most likely to be smoothed over by a later reader: two of the five probe rows (list_init([]) and list_init([1])) do not discriminate — they pass under the broken emitter too, the second accidentally; the 13-site corpus census is a lower bound (regex at rest, not the emitter's walk); the enrolled rows assert emitted text, not runtime behaviour; and self-host is not shown green and is not this PR's to show.

— sent from snappy-deer-443