diff --git a/dag/gunbc/emit_copy_qualification.dag b/dag/gunbc/emit_copy_qualification.dag new file mode 100644 index 00000000000..c9537c27d4e --- /dev/null +++ b/dag/gunbc/emit_copy_qualification.dag @@ -0,0 +1,337 @@ +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)), + ) +} + +// 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" } + } + } +} + +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 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 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: _ } => [copy_cell_clone_site_spelling(cell: cell)] + CloneAbsent => [] + CloneEmittedUndecidable { reason: _ } => [] + CloneEmittedRedundant { receipt: _ } => [] + CloneMinimalityUnobserved => [] + } +} + +fn copy_cell_clone_absent_expectation(cell: CopyQualificationCell) -> List { + match copy_cell_minimality(cell: cell) { + CloneAbsent => [copy_cell_clone_site_spelling(cell: cell)] + 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. +fn copy_cell_expected_present(cell: CopyQualificationCell) -> List { + concat( + concat( + [copy_fixture_anchor(position: cell.position)], + copy_cell_clone_present_expectation(cell: cell), + ), + [copy_receiver_realized_spelling(shape: cell.shape)], + ) +} + +fn copy_cell_expected_absent(cell: CopyQualificationCell) -> List { + concat( + 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 new file mode 100644 index 00000000000..ef7fe809dc8 --- /dev/null +++ b/dag/test/claim/emit_copy_qualification_witness_test.dag @@ -0,0 +1,247 @@ +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, + CopyReceiverShape, + PositionDirectReturn, + PositionDuplicatedArgument, + PositionReturnedClosureCapture, + 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_qualification_population +} + +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. +// +// 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 +// 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), + ) +} + +// 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) +} + +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"], + ["w.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() +} + +// 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), 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), copy_cell_clone_site_spelling(cell: cell)) +} + +fn ecq_cell_forbids_clone(cell: CopyQualificationCell) -> Bool { + contains(copy_cell_expected_absent(cell: cell), copy_cell_clone_site_spelling(cell: cell)) +} + +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 }) +} 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();") }