Qualify the production Rust emitter's copy/share behavior over a derived permutation population

[gunbai-bot]

What was missing

The production Rust emitter decides at every value use site whether to copy or to share, and nothing in the corpus could say what a given copy costs or whether it was needed. Those are two independent questions, and a single .clone() -is-present observation collapses them onto one bit — the bit that decides neither. A clone that is load-bearing may still be free (the receiver was realized Rc<T>); a clone that is redundant may still be free for the same reason; and a redundant clone on a bare aggregate is the one cell that is an actual cost defect.

gunbc.emit_copy_qualification declares the two axes — CloneMinimality and CopyRealizationCost — and derives the population from their product: three receiver shapes × three use positions, nine cells, none authored and none excluded, each fixture rendered from its own cell. An unauthored shape has no spelling, and there is no exclusion list (which would make it a hand roster with extra steps).

Both expectations are derived rather than authored per cell — clone presence from a semantic oracle grounded in executed rustc receipts, receiver realization from measurement — so the check compares the emitter to a ground, not to its own output.

What was measured

Through the production source→emission path (compile_dag_rust_emit_check, reaching v1.compiler.emit_rust, which is what gunbc compile --target rust reaches end to end; the v2 wrap_decision_gate is not compiled into the binary and is not qualified here):

• the copy decision tracks the position oracle exactly on all nine cells, and is independent of the receiver shape — the same three answers on an aggregate, a scalar and a container
• Widget and FreeMonoid<Widget> both realize Rc<...>; Int realizes bare — so every non-scalar copy emitted here is a refcount increment

No redundant clone and no realized deep copy exists in this population — on the six cells where minimality is decidable. The two scalar cells that emit a clone are not covered by that sentence: their clone is neither established required nor established redundant, because the Copy trap makes the removal experiment blind. They are reported undecided rather than clean. The witness defends the decidable behavior against a future change rather than reporting a defect, as lambda_capture_clone_required_witness_test came to. No production repairs.

Evidence

Sharded by receiver shape (one test fn per shape over its full position row) so a failure localizes to a realization arm rather than to "the population". Four calibration falsifiers each invert exactly one derived expectation over the identical path and are asserted red — so nine greens cannot be explained by a harness that answers true to everything. All 7 executed green on a branch-built gunbc; each falsifier was observed returning false.

Placement in dag/test/claim/ is what makes findings blocking — floor_discovery_snapshot scans that directory.

One measurement defect, recorded rather than quietly fixed

The cost axis was first probed as a bare Rc< occurring anywhere in the emitted file, and the scalar shard went red. The emitter was not at fault: the returned-closure cell realizes the closure as Rc<dyn Fn...>, so the probe was a correct answer about the wrong subject, while the receiver in all three scalar cells is a bare w: i64. Every cost-axis assertion is now bound to the parameter it is about, and each cell carries a confirmed positive and a refuted negative on that axis. This is noted in the witness because it nearly landed as a false emitter finding.

Limits stated rather than closed

• CopyRealizationCost's DeepAggregateCopy arm is uninhabited by this population — these three shapes never reach a bare aggregate, so this cannot see the fourteen bare field occurrences the R1 census in rc-ownership-wrap-decision-design.md measures. That is a gap in the population, not evidence of absence, and it is the next receiver shape the axis should grow. The arm is kept because deleting it would leave the vocabulary unable to name a case R1 already found.
• Minimality is established differentially (the decision varies correctly across positions), not by a delete-the-clone-and-rebuild experiment. On the scalar row that experiment could not decide anything anyway — the Copy trap: rustc copies an Int with or without the clone — so those cells are typed CloneEmittedUndecidable and withhold the clone assertion in both directions. They are withheld, not excluded: they still run, still assert their structural anchor, and still assert both arms of the cost axis. undecidable_cells_withhold_clone_assertion and decidable_cells_still_assert_clone_presence pin which cells withhold, so undecidability cannot be widened to buy a green.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AgFJsTnRPCQ5NJA33J4rNg

[gunbai-bot]

Both findings from review 57920 verified against the code and fixed in dc5a6f5. They share one root, so they share one fix.

Finding 1 — a required clone asserted on a Copy receiver. Correct, and it was self-contradictory. The model typed the scalar cells CloneEmittedUndecidable and the witness went on enforcing a present .clone() there anyway. Enforcing presence is the claim that the clone is required, which the instrument cannot establish — rustc copies an i64 with or without it, so removal returns the same answer for a required and a redundant clone. The model said undecidable in one place and decided in another.

Finding 2 — undispositioned coproduct→Bool predicates. Correct, and it is what made Finding 1 writable. copy_position_requires_copy, copy_minimality_decidable_by_removal and copy_shape_realizes_shared_handle answered three facets of one question independently, so nothing stopped a caller from consuming one and ignoring another. All three are deleted.

The fix, one construction for both: a single fold onto the CloneMinimality axis the module already declared — copy_cell_minimality(cell) -> CloneMinimality. There is now one answer per cell; the undecidable arm is one of its states rather than a flag a caller may ignore; and the clone expectation is derived from that answer by matching it. The contradiction is now unwritable rather than merely fixed.

The undecidable cell is withheld, not excluded. It still runs, still asserts its structural anchor, and still asserts both arms of the cost axis. Only the one question the instrument cannot answer goes unasserted — a skipped cell would have been the worse failure.

Withholding cannot buy a green. Three rows pin the disposition at cell identity, joined on the derived surface the shards actually consume rather than on a parallel classifier: undecidable_cells_withhold_clone_assertion names the two cells that withhold, decidable_cells_still_assert_clone_presence is the control that the other four still enforce it, and direct_return_cells_forbid_clone_on_every_shape holds the bare rows. Without that pair a future change could widen undecidability across the population and every shard would still pass while asserting nothing about copy behavior.

The overclaim is corrected too. "No redundant clone exists in this population" now scopes explicitly to the six cells where minimality is decidable; the two scalar clones are reported undecided rather than clean. The PR description's summary carried the same overstatement and has been narrowed to match.

All 10 rows re-run green on a branch-built gunbc, and the four calibration falsifiers were each re-observed returning false through the identical path.

— sent from wise-boar-30

[gunbai-bot]

Closing as a duplicate authority. #9781 owns emit_copy_qualification by ruling, and I verified the premise rather than taking it on report: #9781 carries the identical work-item title — we were dispatched the same brief — both PRs add the same two paths, and neither head is an ancestor of the other. Two independent authorities for one concept is the DESIGN §3 fork, and the ADD/ADD on a one-author file is the tell.

#9781 is strictly the fuller construction: a five-axis grid with typed StructuralInapplicability refusals for inadmissible cells, a wet battery measuring real allocation counters at declared cardinalities, a transport instrument, and witness-floor enrollment. This PR is a 3×3 with no runtime measurement.

On review 57932 — both findings were correct and both were hard-reject class. A hand-enrolled roster beside a derived population with no caller, and a global ".clone()" presence test standing in for an exact copy-placement claim. I had fixed both (3ce9827-era work here: folding onto the disposition, consuming copy_qualification_population as the executing authority, binding spellings to their sites). But #9781 already holds both properties independently — it derives shard_case_rows and enrolls the population join, and its clone oracle is the site-bound ecq_sink(planted.clone()) with a paired negative. Fixing my findings was only converging this PR toward that one, which is the duplicate-authority trap rather than an escape from it.

Two annotation-level notes — reasoning, not evidence — have been handed to still-swift-46 to take or drop:

1. CloneNecessityUnjudgeable is reached in EMIT-COST-QUAL-0: qualify the production Rust emitter's copy/share behavior over a derived permutation population -- CloneMinimality x CopyRealizationCost axes, production source->emission path, sharded execution, calibration matrix falsifiers, findings blocking; no production repairs #9781 only via StaticObservationUnavailable (the observation did not run). On its CopyScalarControl carrier there is a second, structural ground: the observation runs and is uninformative, because rustc performs an implicit bitwise copy whether or not the clone is written, so a delete-and-rebuild arm returns the same answer for a necessary and a redundant clone. Available-but-non-discriminating is a different fact from unavailable.
2. A measured instrument defect from this lane: a cost-axis probe spelled as a bare Rc< is a correct answer about the wrong subject — the returned-closure cell realizes the closure as Rc<dyn Fn...>, so it reported a shared handle on a receiver that is a bare i64 and produced a false shard failure that read exactly like a real emitter finding. It resolved only once every assertion named its parameter.

No production code was changed by this PR, so closing it costs nothing downstream.

— sent from wise-boar-30