From f1fa03de3c79e3b2603e4f1d67c434272995c30e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 31 Aug 2026 18:25:31 +0000 Subject: [PATCH 1/3] Qualify the production Rust emitter's copy/share behavior over a derived permutation population The 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. A single ".clone() is present" observation collapses those two questions onto one bit, and the bit that survives decides neither. gunbc.emit_copy_qualification declares the two axes and derives the population from their product -- three receiver shapes by three use positions, nine cells, none authored and none excluded, each fixture rendered from its cell. Both expectations are derived: clone presence from a semantic oracle grounded in executed rustc receipts, receiver realization from measurement. So the check compares the emitter to a ground rather than to its own output. Measured through the production source->emission path (compile_dag_rust_emit_check, reaching v1.compiler.emit_rust as `gunbc compile --target rust` does; 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 - Widget and FreeMonoid 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, so the witness defends that behavior rather than reporting a defect. No production repairs. Sharded by receiver shape so a failure localizes to a realization arm. Four calibration falsifiers each invert exactly one derived expectation over the identical path and are asserted red, so the greens cannot be explained by an inert harness. Two limits are stated rather than closed: CopyRealizationCost's DeepAggregateCopy arm is uninhabited by this population, which therefore cannot see the fourteen bare field occurrences the R1 census measures; and minimality is established differentially rather than by a delete-and-rebuild experiment, which on the scalar row could not decide anything anyway (the Copy trap), so that cell is typed undecidable rather than reported minimal. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AgFJsTnRPCQ5NJA33J4rNg --- dag/gunbc/emit_copy_qualification.dag | 281 ++++++++++++++++++ .../emit_copy_qualification_witness_test.dag | 153 ++++++++++ 2 files changed, 434 insertions(+) create mode 100644 dag/gunbc/emit_copy_qualification.dag create mode 100644 dag/test/claim/emit_copy_qualification_witness_test.dag diff --git a/dag/gunbc/emit_copy_qualification.dag b/dag/gunbc/emit_copy_qualification.dag new file mode 100644 index 00000000000..c7ae18f36e1 --- /dev/null +++ b/dag/gunbc/emit_copy_qualification.dag @@ -0,0 +1,281 @@ +module gunbc.emit_copy_qualification + +import std.types { Bool, List, NonEmptyStr, String } + +// WHY THIS MODULE EXISTS, in one sentence: 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 -- two different questions that a single ".clone() is present" observation +// silently conflates. +// +// The two axes are independent and neither implies the other. A clone that is load-bearing may +// still be free (the receiver was realized Rc, so the copy is a refcount increment). A clone +// that is redundant may still be free for the same reason. And a clone that is redundant on a bare +// aggregate is the one cell that is an actual cost defect. Reading only clone presence collapses a +// 2-axis space onto one bit, and the bit that survives is the one that does not decide anything. +// +// DISJOINT FROM THE CARRIER-COST VOCABULARY, stated because the names are near neighbours and a +// silent fork here would be exactly DESIGN section 3's failure. std.primitives +// CarrierCostSensitivity and v2.std.value_carrier CarrierCost describe the asymptotics of a +// PERSISTENT COLLECTION CARRIER -- the update and lookup work of a hash-array-mapped trie against a +// relaxed-radix-balanced tree. This module describes what one COPY OF ONE VALUE costs once the Rust +// emitter has chosen a realization for it. Different subject, different authority; a FreeMonoid's +// lookup work is not a fact about what cloning a handle to it costs. +// +// SUBJECT, named so this vocabulary is not read as covering more than it does. The production +// source->Rust-emission path is the v1 seed emitter (v1.compiler.emit_rust), which is what +// `gunbc compile --target rust` reaches end to end; the R1 census in +// docs/plans/rc-ownership-wrap-decision-design.md establishes that the v2 wrap_decision_gate is not +// compiled into the binary and was dormant while the measured sites were produced. v2's +// v2.compiler.use_site_verdict UseSiteVerdict is a DIFFERENT path and is not qualified here. + +// What one copy costs once the emitter has realized the receiver. Grounded in the realization the +// emitter actually chose, not in the authored type: the same authored type reaches Rc at one +// occurrence and bare at another (the fourteen bare field occurrences R1 measured), so the cost is +// a property of the occurrence's realization and cannot be read off the declaration. +type CopyRealizationCost + = ShareHandleBump { realization: NonEmptyStr } + | DeepAggregateCopy { realization: NonEmptyStr } + | MachineWordCopy { realization: NonEmptyStr } + | CopyRealizationUnobserved + +// Whether an emitted copy was needed. CloneEmittedUndecidable is the axis's load-bearing arm and +// not a catch-all: where the receiver is Copy-eligible, rustc performs an implicit bitwise copy +// whether or not the clone is written, so DELETING THE CLONE COMPILES EITHER WAY and the removal +// experiment returns the same answer for a required and a redundant clone. That is a property of +// the experiment, not of the emitter -- the question is genuinely not decidable by that instrument, +// and answering it anyway would be the fabricated plausible output DESIGN section 5 forbids. This +// is the Copy-trap the lambda_capture_clone_required witness names as the reason its own receipt is +// trustworthy rather than vacuous. +// +// CloneMinimalityUnobserved is a different fact with a different remedy: nobody ran the experiment. +// Collapsing it into CloneEmittedRequired would let an unmeasured clone read as defended. +type CloneMinimality + = CloneAbsent + | CloneEmittedRequired { receipt: NonEmptyStr } + | CloneEmittedRedundant { receipt: NonEmptyStr } + | CloneEmittedUndecidable { reason: NonEmptyStr } + | CloneMinimalityUnobserved + +// The receiver shapes the derived population ranges over. Closed, and each is chosen because it +// forces a DIFFERENT arm of CopyRealizationCost out of the emitter -- the axis is the realization +// trichotomy, so a shape that could not distinguish two arms would add a row without adding a +// question. +type CopyReceiverShape + = ReceiverAggregateNonCopy + | ReceiverMachineScalar + | ReceiverSharedContainer + +// The use positions the derived population ranges over. Each is chosen for its KNOWN semantic +// answer, which is what makes a differential over the population informative: a direct return needs +// no copy, and a capture by a returned Fn closure provably does (Arm C, rustc E0507, recorded in +// dag/test/claim/lambda_capture_clone_required_witness_test.dag). A duplicated use needs a copy at +// every use but the last. +type CopyUsePosition + = PositionDirectReturn + | PositionReturnedClosureCapture + | PositionDuplicatedArgument + +data copy_receiver_shapes_all: List = [ + ReceiverAggregateNonCopy, + ReceiverMachineScalar, + ReceiverSharedContainer, +] + +data copy_use_positions_all: List = [ + PositionDirectReturn, + PositionReturnedClosureCapture, + PositionDuplicatedArgument, +] + +// One cell of the derived population. Authored nowhere: cells come from the product below, so a +// shape the axes admit has no way to be left out and no way to be spelled twice. +type CopyQualificationCell { + shape: CopyReceiverShape + position: CopyUsePosition +} + +fn copy_cells_for_shape(shape: CopyReceiverShape) -> List { + map(copy_use_positions_all, p => CopyQualificationCell { shape: shape, position: p }) +} + +// THE POPULATION, derived rather than rostered. An exclusion list here would make this a hand +// roster with extra steps; a cell the emitter cannot yet satisfy is a finding below, never a +// removed row. +fn copy_qualification_population() -> List { + fold( + copy_receiver_shapes_all, + init: [], + f: (acc, s) => concat(acc, copy_cells_for_shape(shape: s)), + ) +} + +// Whether the position semantically REQUIRES a copy, independent of what the emitter did. This is +// the oracle the population is measured against, and it is grounded in executed rustc receipts +// rather than in the emitter's own output -- reading the requirement off the emitter would make the +// check compare the emitter to itself. +fn copy_position_requires_copy(position: CopyUsePosition) -> Bool { + match position { + PositionDirectReturn => false + PositionReturnedClosureCapture => true + PositionDuplicatedArgument => true + } +} + +// THE COPY-TRAP LAW, derived rather than authored per cell: on a Copy-eligible receiver the removal +// experiment cannot discriminate, so minimality is undecidable by it whatever the position. Stating +// this as a derivation is what stops a future author from recording a confident CloneEmittedRedundant +// on a scalar row because the delete-and-rebuild arm happened to compile. +fn copy_minimality_decidable_by_removal(shape: CopyReceiverShape) -> Bool { + match shape { + ReceiverAggregateNonCopy => true + ReceiverMachineScalar => false + ReceiverSharedContainer => true + } +} + +// Whether the emitter realizes this receiver shape as a shared handle. MEASURED, not predicted: +// run through the production source->emission path, Widget and FreeMonoid both render +// Rc<...> at the fn signature and Int renders bare. The consequence is the one that matters for the +// cost axis -- on this population every non-scalar copy the emitter emits is a refcount increment, +// so there is no realized deep copy here at all. +fn copy_shape_realizes_shared_handle(shape: CopyReceiverShape) -> Bool { + match shape { + ReceiverAggregateNonCopy => true + ReceiverMachineScalar => false + ReceiverSharedContainer => true + } +} + +// The cost axis, derived from the measured realization rather than authored per cell. The +// DeepAggregateCopy arm is deliberately reachable in this vocabulary while being UNINHABITED by +// this population, and that gap is stated rather than closed: the R1 census in +// docs/plans/rc-ownership-wrap-decision-design.md measures fourteen bare field occurrences across +// ten types where the wrap misses, so a deep copy is authorable in the real corpus -- these three +// receiver shapes simply do not reach one. Deleting the arm would make the vocabulary unable to +// name the case R1 already found; asserting this population covers it would be the stronger lie. +fn copy_realization_cost_for(shape: CopyReceiverShape) -> CopyRealizationCost { + match shape { + ReceiverAggregateNonCopy => ShareHandleBump { realization: "Rc at fn signature" } + ReceiverMachineScalar => MachineWordCopy { realization: "bare i64 at fn signature" } + ReceiverSharedContainer => ShareHandleBump { realization: "Rc> at fn signature" } + } +} + +fn copy_shape_token(shape: CopyReceiverShape) -> String { + match shape { + ReceiverAggregateNonCopy => "aggregate" + ReceiverMachineScalar => "scalar" + ReceiverSharedContainer => "shared" + } +} + +fn copy_position_token(position: CopyUsePosition) -> String { + match position { + PositionDirectReturn => "direct" + PositionReturnedClosureCapture => "lambda" + PositionDuplicatedArgument => "dup" + } +} + +fn copy_receiver_type_spelling(shape: CopyReceiverShape) -> String { + match shape { + ReceiverAggregateNonCopy => "Widget" + ReceiverMachineScalar => "Int" + ReceiverSharedContainer => "FreeMonoid" + } +} + +fn copy_fixture_header(shape: CopyReceiverShape) -> String { + match shape { + ReceiverAggregateNonCopy => "\n\ntype Widget {\n tag: String\n}\n\n" + ReceiverMachineScalar => "\n\n" + ReceiverSharedContainer => "\nimport std.algebra { FreeMonoid }\n\ntype Widget {\n tag: String\n}\n\n" + } +} + +// The function under emission, one per use position. The anchor name is derived from the same token +// the path is, so a cell cannot assert against a function it did not emit. +fn copy_fixture_body(position: CopyUsePosition, ty: String) -> String { + match position { + PositionDirectReturn => + "fn cell_direct(w: " + ty + ") -> " + ty + " {\n w\n}\n" + PositionReturnedClosureCapture => + "fn cell_lambda(w: " + ty + ") -> fn(Int) -> " + ty + " {\n fn(u) { w }\n}\n" + PositionDuplicatedArgument => + "fn cell_pick(a: " + ty + ", b: " + ty + ") -> " + ty + " {\n a\n}\n\nfn cell_dup(w: " + ty + ") -> " + ty + " {\n cell_pick(w, w)\n}\n" + } +} + +fn copy_cell_slug(cell: CopyQualificationCell) -> String { + copy_shape_token(shape: cell.shape) + "_" + copy_position_token(position: cell.position) +} + +// THE FIXTURE IS DERIVED FROM THE CELL, which is what makes the population a product rather than a +// roster: there is no place to author a source for a cell the axes do not admit, and no way to omit +// one they do. +fn copy_fixture_source(cell: CopyQualificationCell) -> String { + "module emit_copy_qual." + copy_cell_slug(cell: cell) + + copy_fixture_header(shape: cell.shape) + + copy_fixture_body(position: cell.position, ty: copy_receiver_type_spelling(shape: cell.shape)) +} + +fn copy_fixture_path(cell: CopyQualificationCell) -> String { + "src/emit_copy_qual_" + copy_cell_slug(cell: cell) + ".rs" +} + +// A positive structural anchor, always asserted present. Without it a cell whose only assertion is +// an ABSENT .clone() cannot tell a real bare emission from the harness silently emitting nothing -- +// compile_dag_rust_emit_check returns false for a refusal and for a missing file alike. +fn copy_fixture_anchor(position: CopyUsePosition) -> String { + match position { + PositionDirectReturn => "fn cell_direct" + PositionReturnedClosureCapture => "fn cell_lambda" + PositionDuplicatedArgument => "fn cell_dup" + } +} + +// THE RECEIVER-BOUND REALIZATION SPELLING, and the reason it is spelled with the parameter name +// rather than as a bare "Rc<". Asserting "Rc< occurs somewhere in the emitted file" is a correct +// answer about the WRONG SUBJECT: the returned-closure cell realizes the closure itself as +// Rc, so a bare Rc< probe reports present on a scalar receiver whose parameter is a bare +// i64. That is measured, not hypothetical -- it produced a false shard failure before the +// assertions were bound to the receiver. Every cost-axis assertion below therefore names the +// parameter it is about. +fn copy_receiver_realized_spelling(shape: CopyReceiverShape) -> String { + match shape { + ReceiverAggregateNonCopy => "w: Rc" + ReceiverMachineScalar => "w: i64" + ReceiverSharedContainer => "w: Rc<" + } +} + +// The spelling the receiver must NOT carry -- the other arm of the realization it was measured to +// take. Paired with the one above so every cell asserts a confirmed positive and a refuted negative +// on the cost axis, rather than an absence that a silently-empty emission would also satisfy. +fn copy_receiver_refuted_spelling(shape: CopyReceiverShape) -> String { + match shape { + ReceiverAggregateNonCopy => "w: Widget" + ReceiverMachineScalar => "w: Rc<" + ReceiverSharedContainer => "w: FreeMonoid" + } +} + +// The spellings a cell must contain, derived jointly from the semantic oracle (does this position +// require a copy) and the measured realization (how is this receiver realized). Nothing here is +// authored per cell, so the check compares the emitter to a ground rather than to itself. +fn copy_cell_expected_present(cell: CopyQualificationCell) -> List { + concat( + concat( + [copy_fixture_anchor(position: cell.position)], + if copy_position_requires_copy(position: cell.position) { [".clone()"] } else { [] }, + ), + [copy_receiver_realized_spelling(shape: cell.shape)], + ) +} + +fn copy_cell_expected_absent(cell: CopyQualificationCell) -> List { + concat( + if copy_position_requires_copy(position: cell.position) { [] } else { [".clone()"] }, + [copy_receiver_refuted_spelling(shape: cell.shape)], + ) +} diff --git a/dag/test/claim/emit_copy_qualification_witness_test.dag b/dag/test/claim/emit_copy_qualification_witness_test.dag new file mode 100644 index 00000000000..cda8006716e --- /dev/null +++ b/dag/test/claim/emit_copy_qualification_witness_test.dag @@ -0,0 +1,153 @@ +module test.claim.emit_copy_qualification_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.emit_copy_qualification { + CopyQualificationCell, + CopyReceiverShape, + PositionDirectReturn, + PositionDuplicatedArgument, + PositionReturnedClosureCapture, + ReceiverAggregateNonCopy, + ReceiverMachineScalar, + ReceiverSharedContainer, + copy_cell_expected_absent, + copy_cell_expected_present, + copy_cells_for_shape, + copy_fixture_path, + copy_fixture_source +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// Executing floor witness qualifying the PRODUCTION Rust emitter's copy/share behavior over a +// DERIVED population -- the product of gunbc.emit_copy_qualification's two axes, three receiver +// shapes by three use positions, nine cells with no cell authored and no cell excluded. The +// consumer is compile_dag_rust_emit_check, the per-PR enrolled real-emitter arm, so every row runs +// the source->Rust-emission path the `gunbc compile --target rust` binary reaches (v1.compiler. +// emit_rust; the v2 wrap_decision_gate is not compiled into the binary and is not qualified here). +// +// WHAT THIS QUALIFIES, on two axes that a bare ".clone() is present" observation collapses into +// one. CloneMinimality: the emitter must emit a copy exactly where the position semantically needs +// one -- bare on a direct return, cloned into a returned closure's capture and at a duplicated +// argument. CopyRealizationCost: what that copy costs once realized. Both expectations are DERIVED +// in the model from a semantic oracle and a measured realization, never authored per cell, so the +// check compares the emitter to a ground rather than to its own output. +// +// THE MEASURED RESULT THIS LOCKS IN, and it is a qualification rather than an indictment: over all +// nine cells the emitter's copy decision tracks the position oracle exactly, and it is INDEPENDENT +// of the receiver shape -- the same three answers on an aggregate, a scalar and a container. On the +// cost axis Widget and FreeMonoid both realize Rc<...> while 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. This file therefore defends that behavior against a future change +// rather than reporting a defect, exactly as lambda_capture_clone_required_witness_test came to. +// +// WHAT IT DOES NOT ESTABLISH, stated so the greens are not read wider than they reach. The +// DeepAggregateCopy arm of CopyRealizationCost is UNINHABITED here: these three shapes never reach +// a bare aggregate, so this population cannot see the fourteen bare field occurrences the R1 census +// in docs/plans/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 this axis should grow. Minimality is +// established DIFFERENTIALLY -- the emitter's 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), which is why the +// model types that cell undecidable rather than reporting it minimal. +// +// ONE MEASUREMENT DEFECT IS RECORDED HERE because it nearly landed as an emitter finding. 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, 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. + +// SHARDED BY RECEIVER SHAPE, one test fn per shape over that shape's full position row, so a +// failure localizes to a realization arm instead of to "the population", and the three shards run +// independently. + +fn ecq_cell_holds(cell: CopyQualificationCell) -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: cell), + copy_fixture_path(cell: cell), + copy_cell_expected_present(cell: cell), + copy_cell_expected_absent(cell: cell) + ) +} + +fn ecq_shard_holds(shape: CopyReceiverShape) -> Bool { + fold( + copy_cells_for_shape(shape: shape), + init: true, + f: (acc, cell) => acc && ecq_cell_holds(cell: cell), + ) +} + +test fn shard_aggregate_non_copy_receiver() -> Bool { + ecq_shard_holds(shape: ReceiverAggregateNonCopy) +} + +test fn shard_machine_scalar_receiver() -> Bool { + ecq_shard_holds(shape: ReceiverMachineScalar) +} + +test fn shard_shared_container_receiver() -> Bool { + ecq_shard_holds(shape: ReceiverSharedContainer) +} + +// THE CALIBRATION MATRIX. Nine greens from an instrument never observed to go red are not a +// measurement, and each falsifier below inverts exactly ONE derived expectation while running the +// identical path, so a green shard cannot be explained by the harness answering true to everything. +// +// Each falsifier asserts the NEGATION of a measured fact and must therefore return false; a test fn +// wrapping it asserts that it does. If the emitter's behavior changes, the matching shard reddens +// AND its falsifier greens -- two independent signals, which is what separates a real behavior +// change from the harness having gone inert. + +fn ecq_falsifier_direct_return_clones() -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionDirectReturn }), + copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionDirectReturn }), + ["fn cell_direct", ".clone()"], + [] + ) +} + +fn ecq_falsifier_closure_capture_is_bare() -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionReturnedClosureCapture }), + copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionReturnedClosureCapture }), + ["fn cell_lambda"], + [".clone()"] + ) +} + +fn ecq_falsifier_scalar_realizes_shared_handle() -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverMachineScalar, position: PositionDirectReturn }), + copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverMachineScalar, position: PositionDirectReturn }), + ["fn cell_direct", "w: Rc<"], + [] + ) +} + +fn ecq_falsifier_container_realizes_bare() -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverSharedContainer, position: PositionDuplicatedArgument }), + copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverSharedContainer, position: PositionDuplicatedArgument }), + ["fn cell_dup"], + ["w: Rc<"] + ) +} + +test fn calibration_direct_return_clone_falsifier_is_red() -> Bool { + !ecq_falsifier_direct_return_clones() +} + +test fn calibration_closure_capture_bare_falsifier_is_red() -> Bool { + !ecq_falsifier_closure_capture_is_bare() +} + +test fn calibration_scalar_shared_handle_falsifier_is_red() -> Bool { + !ecq_falsifier_scalar_realizes_shared_handle() +} + +test fn calibration_container_bare_falsifier_is_red() -> Bool { + !ecq_falsifier_container_realizes_bare() +} From 152e84042b7ce3a968238d4d4966b1f38db1080d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 31 Aug 2026 18:58:34 +0000 Subject: [PATCH 2/3] Fold the copy/share predicates onto CloneMinimality; stop asserting a required clone on Copy receivers Both findings from review 57920 share one root and one fix. The model typed the scalar cells CloneEmittedUndecidable and the witness went on enforcing a present .clone() there anyway -- which asserts the clone is REQUIRED, a stronger result than the instrument can decide, since rustc copies an i64 with or without it. Three separate coproduct-to-Bool predicates are what allowed that: "does this position require a copy", "is minimality decidable here" and "is this receiver a shared handle" were answered independently, so nothing stopped a caller from consuming one and ignoring another. Folding once onto CloneMinimality makes the contradiction unwritable. There is 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. 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. Three rows pin the disposition at cell identity so withholding cannot become a way to buy a green -- undecidable_cells_withhold_clone_assertion names the two cells that withhold, and decidable_cells_still_assert_clone_presence is the control that the other four still enforce it. Without the pair, a future change could widen undecidability across the population and every shard would still pass while asserting nothing about copy behavior at all. The header's "no redundant clone in this population" is corrected to scope to the six cells where minimality is decidable; the two scalar clones are reported undecided rather than clean. All 10 rows re-run green on a branch-built gunbc; the four calibration falsifiers were each re-observed returning false. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01AgFJsTnRPCQ5NJA33J4rNg --- dag/gunbc/emit_copy_qualification.dag | 133 +++++++++++------- .../emit_copy_qualification_witness_test.dag | 52 ++++++- 2 files changed, 131 insertions(+), 54 deletions(-) diff --git a/dag/gunbc/emit_copy_qualification.dag b/dag/gunbc/emit_copy_qualification.dag index c7ae18f36e1..f2e97c32b27 100644 --- a/dag/gunbc/emit_copy_qualification.dag +++ b/dag/gunbc/emit_copy_qualification.dag @@ -109,55 +109,55 @@ fn copy_qualification_population() -> List { ) } -// Whether the position semantically REQUIRES a copy, independent of what the emitter did. This is -// the oracle the population is measured against, and it is grounded in executed rustc receipts -// rather than in the emitter's own output -- reading the requirement off the emitter would make the -// check compare the emitter to itself. -fn copy_position_requires_copy(position: CopyUsePosition) -> Bool { - match position { - PositionDirectReturn => false - PositionReturnedClosureCapture => true - PositionDuplicatedArgument => true - } -} - -// THE COPY-TRAP LAW, derived rather than authored per cell: on a Copy-eligible receiver the removal -// experiment cannot discriminate, so minimality is undecidable by it whatever the position. Stating -// this as a derivation is what stops a future author from recording a confident CloneEmittedRedundant -// on a scalar row because the delete-and-rebuild arm happened to compile. -fn copy_minimality_decidable_by_removal(shape: CopyReceiverShape) -> Bool { - match shape { - ReceiverAggregateNonCopy => true - ReceiverMachineScalar => false - ReceiverSharedContainer => true - } -} - -// Whether the emitter realizes this receiver shape as a shared handle. MEASURED, not predicted: -// run through the production source->emission path, Widget and FreeMonoid both render -// Rc<...> at the fn signature and Int renders bare. The consequence is the one that matters for the -// cost axis -- on this population every non-scalar copy the emitter emits is a refcount increment, -// so there is no realized deep copy here at all. -fn copy_shape_realizes_shared_handle(shape: CopyReceiverShape) -> Bool { - match shape { - ReceiverAggregateNonCopy => true - ReceiverMachineScalar => false - ReceiverSharedContainer => true - } -} - -// The cost axis, derived from the measured realization rather than authored per cell. The -// DeepAggregateCopy arm is deliberately reachable in this vocabulary while being UNINHABITED by -// this population, and that gap is stated rather than closed: the R1 census in -// docs/plans/rc-ownership-wrap-decision-design.md measures fourteen bare field occurrences across -// ten types where the wrap misses, so a deep copy is authorable in the real corpus -- these three -// receiver shapes simply do not reach one. Deleting the arm would make the vocabulary unable to -// name the case R1 already found; asserting this population covers it would be the stronger lie. -fn copy_realization_cost_for(shape: CopyReceiverShape) -> CopyRealizationCost { - match shape { - ReceiverAggregateNonCopy => ShareHandleBump { realization: "Rc at fn signature" } - ReceiverMachineScalar => MachineWordCopy { realization: "bare i64 at fn signature" } - ReceiverSharedContainer => ShareHandleBump { realization: "Rc> at fn signature" } +// THE FOLD TO THE DISPOSITION, replacing three separate coproduct-to-Bool predicates that used to +// answer "does this position require a copy", "is minimality decidable by removal here" and "is +// this receiver a shared handle". Each was a hand-rolled match over a closed coproduct producing a +// bare Bool, none consumed a canonical surface, and -- worse -- they let the two questions be +// answered INDEPENDENTLY, which is how the witness came to assert a required clone on a receiver +// the same model typed undecidable. Folding once onto CloneMinimality makes that contradiction +// unwritable: there is one answer per cell and the undecidable arm is one of its states, not a +// separate flag a caller may ignore. +// +// The oracle is grounded in executed rustc receipts, not in the emitter's output: a direct return +// needs no copy; a capture by a returned Fn closure provably does (Arm C, rustc E0507, recorded in +// dag/test/claim/lambda_capture_clone_required_witness_test.dag); a duplicated argument needs one at +// every use but the last. +// +// THE COPY TRAP IS THE SHAPE ARM, and it is why this is keyed on the cell rather than the position. +// Where the receiver is Copy-eligible, rustc performs an implicit bitwise copy whether or not the +// clone is written, so an EMITTED clone cannot be established as required -- the removal experiment +// returns the same answer for a required and a redundant one. That is a property of the instrument, +// not of the emitter. Note the arm is reached only where a clone is actually emitted: a scalar +// direct return emits none, and CloneAbsent is decidable by direct observation. +fn copy_cell_minimality(cell: CopyQualificationCell) -> CloneMinimality { + match cell.position { + PositionDirectReturn => CloneAbsent + PositionReturnedClosureCapture => + match cell.shape { + ReceiverMachineScalar => + CloneEmittedUndecidable { + reason: "Copy-eligible receiver: rustc copies i64 with or without the clone, so removal cannot discriminate required from redundant", + } + ReceiverAggregateNonCopy => + CloneEmittedRequired { + receipt: "returned Fn closure capture, rustc E0507 on removal (Arm C, lambda_capture_clone_required_witness)", + } + ReceiverSharedContainer => + CloneEmittedRequired { + receipt: "returned Fn closure capture, rustc E0507 on removal (Arm C, lambda_capture_clone_required_witness)", + } + } + PositionDuplicatedArgument => + match cell.shape { + ReceiverMachineScalar => + CloneEmittedUndecidable { + reason: "Copy-eligible receiver: rustc copies i64 with or without the clone, so removal cannot discriminate required from redundant", + } + ReceiverAggregateNonCopy => + CloneEmittedRequired { receipt: "non-Copy receiver consumed at more than one argument position" } + ReceiverSharedContainer => + CloneEmittedRequired { receipt: "non-Copy receiver consumed at more than one argument position" } + } } } @@ -260,6 +260,37 @@ fn copy_receiver_refuted_spelling(shape: CopyReceiverShape) -> String { } } +// THE CLONE EXPECTATION, derived from the cell's disposition so that an undecidable cell asserts +// NOTHING about clone presence in either direction. This is the finding codex/gpt-5.6-sol raised on +// review 57920 and it was correct: the model typed the scalar cells undecidable while the witness +// went on enforcing a present .clone() there, which claims the clone is REQUIRED -- a stronger +// result than the instrument can decide, and exactly the fabricated plausible output DESIGN section +// 5 forbids. +// +// 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, and undecidable_cells_withhold_clone_assertion in the witness pins which +// cells those are, so a future change cannot widen undecidability to buy a green. +fn copy_cell_clone_present_expectation(cell: CopyQualificationCell) -> List { + match copy_cell_minimality(cell: cell) { + CloneEmittedRequired { receipt: _ } => [".clone()"] + CloneAbsent => [] + CloneEmittedUndecidable { reason: _ } => [] + CloneEmittedRedundant { receipt: _ } => [] + CloneMinimalityUnobserved => [] + } +} + +fn copy_cell_clone_absent_expectation(cell: CopyQualificationCell) -> List { + match copy_cell_minimality(cell: cell) { + CloneAbsent => [".clone()"] + CloneEmittedRequired { receipt: _ } => [] + CloneEmittedUndecidable { reason: _ } => [] + CloneEmittedRedundant { receipt: _ } => [] + CloneMinimalityUnobserved => [] + } +} + // The spellings a cell must contain, derived jointly from the semantic oracle (does this position // require a copy) and the measured realization (how is this receiver realized). Nothing here is // authored per cell, so the check compares the emitter to a ground rather than to itself. @@ -267,7 +298,7 @@ fn copy_cell_expected_present(cell: CopyQualificationCell) -> List { concat( concat( [copy_fixture_anchor(position: cell.position)], - if copy_position_requires_copy(position: cell.position) { [".clone()"] } else { [] }, + copy_cell_clone_present_expectation(cell: cell), ), [copy_receiver_realized_spelling(shape: cell.shape)], ) @@ -275,7 +306,7 @@ fn copy_cell_expected_present(cell: CopyQualificationCell) -> List { fn copy_cell_expected_absent(cell: CopyQualificationCell) -> List { concat( - if copy_position_requires_copy(position: cell.position) { [] } else { [".clone()"] }, + copy_cell_clone_absent_expectation(cell: cell), [copy_receiver_refuted_spelling(shape: cell.shape)], ) } diff --git a/dag/test/claim/emit_copy_qualification_witness_test.dag b/dag/test/claim/emit_copy_qualification_witness_test.dag index cda8006716e..712b6696133 100644 --- a/dag/test/claim/emit_copy_qualification_witness_test.dag +++ b/dag/test/claim/emit_copy_qualification_witness_test.dag @@ -37,9 +37,15 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // nine cells the emitter's copy decision tracks the position oracle exactly, and it is INDEPENDENT // of the receiver shape -- the same three answers on an aggregate, a scalar and a container. On the // cost axis Widget and FreeMonoid both realize Rc<...> while 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. This file therefore defends that behavior against a future change -// rather than reporting a defect, exactly as lambda_capture_clone_required_witness_test came to. +// non-scalar copy emitted here is a refcount increment. +// +// SCOPED PRECISELY, because the obvious summary overstates it: no redundant clone and no realized +// deep copy exists in this population ON THE SHAPES WHERE MINIMALITY IS DECIDABLE -- the six +// non-scalar cells. 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 (see copy_cell_minimality). This file defends the decidable behavior +// against a future change, exactly as lambda_capture_clone_required_witness_test came to, and +// reports the rest as undecided rather than as clean. // // WHAT IT DOES NOT ESTABLISH, stated so the greens are not read wider than they reach. The // DeepAggregateCopy arm of CopyRealizationCost is UNINHABITED here: these three shapes never reach @@ -151,3 +157,43 @@ test fn calibration_scalar_shared_handle_falsifier_is_red() -> Bool { test fn calibration_container_bare_falsifier_is_red() -> Bool { !ecq_falsifier_container_realizes_bare() } + +// THE UNDECIDABILITY IS ITSELF UNDER TEST, so that withholding an assertion cannot become a way to +// buy a green. Without this row a future change could widen CloneEmittedUndecidable across the +// population and every shard would still pass while asserting nothing about copy behavior at all -- +// the withheld cell would have degraded into a silently excluded one. +// +// This joins on the derived surface the shards actually consume rather than on a parallel +// classifier, so the two cannot drift: a cell is undecided exactly when neither expectation list +// mentions .clone(). Asserted at cell identity, not by counting. + +fn ecq_cell_withholds_clone(cell: CopyQualificationCell) -> Bool { + !contains(copy_cell_expected_present(cell: cell), ".clone()") + && !contains(copy_cell_expected_absent(cell: cell), ".clone()") +} + +fn ecq_cell_requires_clone(cell: CopyQualificationCell) -> Bool { + contains(copy_cell_expected_present(cell: cell), ".clone()") +} + +fn ecq_cell_forbids_clone(cell: CopyQualificationCell) -> Bool { + contains(copy_cell_expected_absent(cell: cell), ".clone()") +} + +test fn undecidable_cells_withhold_clone_assertion() -> Bool { + ecq_cell_withholds_clone(cell: CopyQualificationCell { shape: ReceiverMachineScalar, position: PositionReturnedClosureCapture }) + && ecq_cell_withholds_clone(cell: CopyQualificationCell { shape: ReceiverMachineScalar, position: PositionDuplicatedArgument }) +} + +test fn decidable_cells_still_assert_clone_presence() -> Bool { + ecq_cell_requires_clone(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionReturnedClosureCapture }) + && ecq_cell_requires_clone(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionDuplicatedArgument }) + && ecq_cell_requires_clone(cell: CopyQualificationCell { shape: ReceiverSharedContainer, position: PositionReturnedClosureCapture }) + && ecq_cell_requires_clone(cell: CopyQualificationCell { shape: ReceiverSharedContainer, position: PositionDuplicatedArgument }) +} + +test fn direct_return_cells_forbid_clone_on_every_shape() -> Bool { + ecq_cell_forbids_clone(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionDirectReturn }) + && ecq_cell_forbids_clone(cell: CopyQualificationCell { shape: ReceiverMachineScalar, position: PositionDirectReturn }) + && ecq_cell_forbids_clone(cell: CopyQualificationCell { shape: ReceiverSharedContainer, position: PositionDirectReturn }) +} From de426e6ab5255de7e7ba2561fa410e77d3a7da28 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 31 Aug 2026 21:06:21 +0000 Subject: [PATCH 3/3] WIP: EMIT-COST-QUAL-0: qualify the production Rust emitter's copy/share behav --- dag/gunbc/emit_copy_qualification.dag | 29 ++++++++- .../emit_copy_qualification_witness_test.dag | 60 +++++++++++++++++-- .../claim/emit_copy_spelling_probe_test.dag | 29 +++++++++ 3 files changed, 110 insertions(+), 8 deletions(-) create mode 100644 dag/test/claim/emit_copy_spelling_probe_test.dag diff --git a/dag/gunbc/emit_copy_qualification.dag b/dag/gunbc/emit_copy_qualification.dag index f2e97c32b27..c9537c27d4e 100644 --- a/dag/gunbc/emit_copy_qualification.dag +++ b/dag/gunbc/emit_copy_qualification.dag @@ -267,13 +267,38 @@ fn copy_receiver_refuted_spelling(shape: CopyReceiverShape) -> String { // result than the instrument can decide, and exactly the fabricated plausible output DESIGN section // 5 forbids. // +// THE SPELLINGS ARE SITE-BOUND, NOT A GLOBAL ".clone()" SUBSTRING, which is the second finding +// (review 57932) and it was correct for the same reason the cost axis needed binding: a bare +// ".clone()" occurring anywhere in the emitted file is satisfied by an unrelated or wrongly placed +// clone, so it cannot establish the "copies exactly where needed" claim the header makes. Each arm +// now names the expression it is about: +// +// direct return -- asserts ".clone()" ABSENT FROM THE WHOLE FILE, which is the strongest +// count statement available: exactly zero copies, not merely none at a +// named site. +// duplicated argument -- asserts the whole call "cell_pick(w.clone(), w)", which pins placement +// AND count together: the copy is on the first argument and the second is +// bare, so a second clone would falsify it. +// closure capture -- asserts the receiver-bound "w.clone()". Placement is bound to the +// receiver; the emitter's closure prelude spelling is not pinned here, so +// this arm bounds WHERE the copy is, not how many times the closure body +// might mention it. Stated rather than claimed as exact. +// // 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, and undecidable_cells_withhold_clone_assertion in the witness pins which // cells those are, so a future change cannot widen undecidability to buy a green. +fn copy_cell_clone_site_spelling(cell: CopyQualificationCell) -> String { + match cell.position { + PositionDirectReturn => ".clone()" + PositionReturnedClosureCapture => "w.clone()" + PositionDuplicatedArgument => "cell_pick(w.clone(), w)" + } +} + fn copy_cell_clone_present_expectation(cell: CopyQualificationCell) -> List { match copy_cell_minimality(cell: cell) { - CloneEmittedRequired { receipt: _ } => [".clone()"] + CloneEmittedRequired { receipt: _ } => [copy_cell_clone_site_spelling(cell: cell)] CloneAbsent => [] CloneEmittedUndecidable { reason: _ } => [] CloneEmittedRedundant { receipt: _ } => [] @@ -283,7 +308,7 @@ fn copy_cell_clone_present_expectation(cell: CopyQualificationCell) -> List List { match copy_cell_minimality(cell: cell) { - CloneAbsent => [".clone()"] + CloneAbsent => [copy_cell_clone_site_spelling(cell: cell)] CloneEmittedRequired { receipt: _ } => [] CloneEmittedUndecidable { reason: _ } => [] CloneEmittedRedundant { receipt: _ } => [] diff --git a/dag/test/claim/emit_copy_qualification_witness_test.dag b/dag/test/claim/emit_copy_qualification_witness_test.dag index 712b6696133..ef7fe809dc8 100644 --- a/dag/test/claim/emit_copy_qualification_witness_test.dag +++ b/dag/test/claim/emit_copy_qualification_witness_test.dag @@ -1,5 +1,6 @@ module test.claim.emit_copy_qualification_witness +import std.types { Bool, List, String } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import gunbc.emit_copy_qualification { CopyQualificationCell, @@ -10,11 +11,14 @@ import gunbc.emit_copy_qualification { ReceiverAggregateNonCopy, ReceiverMachineScalar, ReceiverSharedContainer, + copy_cell_clone_site_spelling, copy_cell_expected_absent, copy_cell_expected_present, + copy_cell_slug, copy_cells_for_shape, copy_fixture_path, - copy_fixture_source + copy_fixture_source, + copy_qualification_population } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -85,6 +89,50 @@ fn ecq_shard_holds(shape: CopyReceiverShape) -> Bool { ) } +// THE POPULATION IS THE EXECUTING AUTHORITY, and the shards sit beneath it. Enrolling one test fn +// per shape and nothing else made copy_qualification_population a function with no caller: the +// shards hand-named three shapes, so a fourth added to the axis would have gone unexecuted while +// every row stayed green -- a derived population that nothing derives from is a hand roster with +// extra steps, which is the exact failure the population was built to avoid. +// +// This row consumes the derived product directly, so coverage is structural: a cell the axes admit +// is executed because it is in the list, not because someone remembered to enrol it. The three +// shape shards below remain because a single total row localizes nothing -- they say WHICH +// realization arm broke. They are diagnostics under this row, never the coverage authority, and +// shards_cover_every_derived_cell pins that they have not drifted from it. +test fn all_derived_cells_hold() -> Bool { + fold( + copy_qualification_population(), + init: true, + f: (acc, cell) => acc && ecq_cell_holds(cell: cell), + ) +} + +fn ecq_shard_enrolled_cells() -> List { + concat( + concat( + copy_cells_for_shape(shape: ReceiverAggregateNonCopy), + copy_cells_for_shape(shape: ReceiverMachineScalar), + ), + copy_cells_for_shape(shape: ReceiverSharedContainer), + ) +} + +// Joined at cell identity rather than by counting, so a shard that swapped one cell for another +// cannot pass on a matching total. +test fn shards_cover_every_derived_cell() -> Bool { + fold( + copy_qualification_population(), + init: true, + f: (acc, cell) => + acc + && contains( + map(ecq_shard_enrolled_cells(), e => copy_cell_slug(cell: e)), + copy_cell_slug(cell: cell), + ), + ) +} + test fn shard_aggregate_non_copy_receiver() -> Bool { ecq_shard_holds(shape: ReceiverAggregateNonCopy) } @@ -120,7 +168,7 @@ fn ecq_falsifier_closure_capture_is_bare() -> Bool { copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionReturnedClosureCapture }), copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: PositionReturnedClosureCapture }), ["fn cell_lambda"], - [".clone()"] + ["w.clone()"] ) } @@ -168,16 +216,16 @@ test fn calibration_container_bare_falsifier_is_red() -> Bool { // mentions .clone(). Asserted at cell identity, not by counting. fn ecq_cell_withholds_clone(cell: CopyQualificationCell) -> Bool { - !contains(copy_cell_expected_present(cell: cell), ".clone()") - && !contains(copy_cell_expected_absent(cell: cell), ".clone()") + !contains(copy_cell_expected_present(cell: cell), copy_cell_clone_site_spelling(cell: cell)) + && !contains(copy_cell_expected_absent(cell: cell), copy_cell_clone_site_spelling(cell: cell)) } fn ecq_cell_requires_clone(cell: CopyQualificationCell) -> Bool { - contains(copy_cell_expected_present(cell: cell), ".clone()") + contains(copy_cell_expected_present(cell: cell), copy_cell_clone_site_spelling(cell: cell)) } fn ecq_cell_forbids_clone(cell: CopyQualificationCell) -> Bool { - contains(copy_cell_expected_absent(cell: cell), ".clone()") + contains(copy_cell_expected_absent(cell: cell), copy_cell_clone_site_spelling(cell: cell)) } test fn undecidable_cells_withhold_clone_assertion() -> Bool { diff --git a/dag/test/claim/emit_copy_spelling_probe_test.dag b/dag/test/claim/emit_copy_spelling_probe_test.dag new file mode 100644 index 00000000000..c0d54de63e7 --- /dev/null +++ b/dag/test/claim/emit_copy_spelling_probe_test.dag @@ -0,0 +1,29 @@ +module test.claim.emit_copy_spelling_probe + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.emit_copy_qualification { + CopyUsePosition, + CopyQualificationCell, + PositionDuplicatedArgument, + PositionReturnedClosureCapture, + ReceiverAggregateNonCopy, + copy_fixture_path, + copy_fixture_source +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn sp(position: CopyUsePosition, spelling: String) -> Bool { + compile_dag_rust_emit_check( + copy_fixture_source(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: position }), + copy_fixture_path(cell: CopyQualificationCell { shape: ReceiverAggregateNonCopy, position: position }), + [spelling], + [] + ) +} + +test fn sp_dup_pick_wclone_w() -> Bool { sp(position: PositionDuplicatedArgument, spelling: "cell_pick(w.clone(), w)") } +test fn sp_dup_wclone() -> Bool { sp(position: PositionDuplicatedArgument, spelling: "w.clone()") } +test fn sp_dup_both_clone() -> Bool { sp(position: PositionDuplicatedArgument, spelling: "cell_pick(w.clone(), w.clone())") } +test fn sp_lambda_wclone() -> Bool { sp(position: PositionReturnedClosureCapture, spelling: "w.clone()") } +test fn sp_lambda_let_prelude() -> Bool { sp(position: PositionReturnedClosureCapture, spelling: "let w = w.clone();") }